src/ZF/Univ.thy

--- a/src/ZF/Univ.thy	Fri Oct 17 17:39:04 1997 +0200
+++ b/src/ZF/Univ.thy	Fri Oct 17 17:40:02 1997 +0200
@@ -12,6 +12,9 @@
 *)
 
 Univ = Arith + Sum + Finite + mono +
+
+global
+
 consts
     Vfrom       :: [i,i]=>i
     Vset        :: i=>i
@@ -21,6 +24,8 @@
 translations
     "Vset(x)"   ==      "Vfrom(0,x)"
 
+path Univ
+
 defs
     Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"