From 4b05e70762dff560e4c5b06e75d8ee61a0ea8fab Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Fri, 1 Aug 2014 11:15:35 -0700 Subject: [PATCH] feat(library/standard/logic/axioms): add import default --- library/standard/logic/axioms/default.lean | 8 ++++++++ library/standard/logic/axioms/hilbert.lean | 3 ++- 2 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 library/standard/logic/axioms/default.lean diff --git a/library/standard/logic/axioms/default.lean b/library/standard/logic/axioms/default.lean new file mode 100644 index 000000000..0c549c505 --- /dev/null +++ b/library/standard/logic/axioms/default.lean @@ -0,0 +1,8 @@ +---------------------------------------------------------------------------------------------------- +--- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +--- Released under Apache 2.0 license as described in the file LICENSE. +--- Author: Jeremy Avigad +---------------------------------------------------------------------------------------------------- + +import logic.axioms.classical logic.axioms.funext logic.axioms.hilbert logic.axioms.piext +import logic.axioms.prop_decidable \ No newline at end of file diff --git a/library/standard/logic/axioms/hilbert.lean b/library/standard/logic/axioms/hilbert.lean index 457e08f39..f45e15c00 100644 --- a/library/standard/logic/axioms/hilbert.lean +++ b/library/standard/logic/axioms/hilbert.lean @@ -1,4 +1,5 @@ ------------------------------------------------------------------------------------------------------- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +---------------------------------------------------------------------------------------------------- +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura ----------------------------------------------------------------------------------------------------