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