--- 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