# HG changeset patch
# User wenzelm
# Date 877008786 -7200
# Node ID 5ae0e1324c563d169f0e268138af03dcc8cebccb
# Parent  4bbfbb7a2cd3ff716251d99d1d246d49853d9934
global;

diff -r 4bbfbb7a2cd3 -r 5ae0e1324c56 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
-
diff -r 4bbfbb7a2cd3 -r 5ae0e1324c56 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Thu Oct 16 15:31:12 1997 +0200
+++ b/src/ZF/ZF.thy	Thu Oct 16 15:33:06 1997 +0200
@@ -8,6 +8,8 @@
 
 ZF = FOL + Let + 
 
+global
+
 types
   i
 
@@ -164,6 +166,9 @@
   subset_def    "A <= B == ALL x:A. x:B"
   succ_def      "succ(i) == cons(i, i)"
 
+
+path ZF
+
 rules
 
   (* ZF axioms -- see Suppes p.238