aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Base.thy
diff options
context:
space:
mode:
Diffstat (limited to 'HoTT_Base.thy')
-rw-r--r--HoTT_Base.thy4
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