src/FOL/IFOL.thy
changeset 9886 897d6602cbfb
parent 9526 e20323caff47
child 11677 ee12f18599e5
--- a/src/FOL/IFOL.thy	Thu Sep 07 20:47:34 2000 +0200
+++ b/src/FOL/IFOL.thy	Thu Sep 07 20:47:54 2000 +0200
@@ -116,10 +116,11 @@
   iff_reflection: "(P<->Q) ==> (P==Q)"
 
 
-			setup Simplifier.setup
-use "IFOL_lemmas.ML"	setup attrib_setup
+setup Simplifier.setup
+use "IFOL_lemmas.ML"
 use "fologic.ML"
-use "hypsubstdata.ML"   setup hypsubst_setup
+use "hypsubstdata.ML"
+setup hypsubst_setup
 use "intprover.ML"