diff options
| author | Josh Chen | 2018-09-18 03:04:37 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-09-18 03:04:37 +0200 |
| commit | dcf87145a1059659099bbecde55973de0d36d43f (patch) | |
| tree | 03707f3dc962e6b762890cff92cb106834b879bc /HoTT_Base.thy | |
| parent | 49c008ef405ab8d8229ae1d5b0737339ee46e576 (diff) | |
Theories fully reorganized. Well-formedness rules removed. New methods etc.
Diffstat (limited to 'HoTT_Base.thy')
| -rw-r--r-- | HoTT_Base.thy | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 17e3142..7453883 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -7,9 +7,7 @@ Basic setup of a homotopy type theory object logic with a cumulative Russell-sty *) theory HoTT_Base -imports - Pure - "HOL-Eisbach.Eisbach" +imports Pure "HOL-Eisbach.Eisbach" begin |