--- a/src/FOL/FOL.thy Wed Aug 25 20:42:01 1999 +0200
+++ b/src/FOL/FOL.thy Wed Aug 25 20:45:19 1999 +0200
@@ -1,10 +1,14 @@
-FOL = IFOL +
+theory FOL = IFOL
+files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("FOL_lemmas2.ML"):
-rules
- classical "(~P ==> P) ==> P"
+axioms
+ classical: "(~P ==> P) ==> P"
-setup ClasetThyData.setup
-setup attrib_setup (* FIXME move to IFOL.thy *)
+use "FOL_lemmas1.ML"
+use "cladata.ML" setup Cla.setup setup clasetup
+use "blastdata.ML" setup Blast.setup
+use "FOL_lemmas2.ML"
+use "simpdata.ML" setup simpsetup setup Clasimp.setup
end