--- a/src/FOL/IFOL.thy Sun Jan 30 20:48:50 2005 +0100
+++ b/src/FOL/IFOL.thy Tue Feb 01 18:01:57 2005 +0100
@@ -5,8 +5,10 @@
header {* Intuitionistic first-order logic *}
-theory IFOL = Pure
-files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML"):
+theory IFOL
+imports Pure
+files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML")
+begin
subsection {* Syntax and axiomatic basis *}
@@ -268,8 +270,6 @@
mp
trans
-
-
subsection {* ``Let'' declarations *}
nonterminals letbinds letbind