--- a/src/FOL/FOL.thy Mon Nov 03 12:26:45 1997 +0100
+++ b/src/FOL/FOL.thy Mon Nov 03 12:26:58 1997 +0100
@@ -1,4 +1,9 @@
+
FOL = IFOL +
+
rules
-classical "(~P ==> P) ==> P"
+ classical "(~P ==> P) ==> P"
+
end
+
+ML val thy_data = [ClasetThyData.thy_data];