src/FOL/IFOL.thy

--- a/src/FOL/IFOL.thy	Thu Oct 16 15:31:12 1997 +0200
+++ b/src/FOL/IFOL.thy	Thu Oct 16 15:33:06 1997 +0200
@@ -8,6 +8,8 @@
 
 IFOL = Pure +
 
+global
+
 classes
   term < logic
 
@@ -62,6 +64,8 @@
   "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
 
 
+path IFOL
+
 rules
 
   (* Equality *)
@@ -108,4 +112,3 @@
   iff_reflection  "(P<->Q) ==> (P==Q)"
 
 end
-