michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/standard/logic/axioms): add import default

Browse source
This commit is contained in:
Jeremy Avigad 2014-08-01 11:15:35 -07:00 committed by Leonardo de Moura
parent 77931f2af8
commit 4b05e70762
2 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/standard/logic/axioms/default.lean Normal file
View file

@ -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

3
library/standard/logic/axioms/hilbert.lean
View file

@ -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
----------------------------------------------------------------------------------------------------