From dcf87145a1059659099bbecde55973de0d36d43f Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 18 Sep 2018 03:04:37 +0200 Subject: Theories fully reorganized. Well-formedness rules removed. New methods etc. --- HoTT_Base.thy | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'HoTT_Base.thy') 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 -- cgit v1.2.3