src/ZF/Univ.thy
changeset 435 ca5356bd315a
parent 124 858ab9a9b047
child 490 e6f0214ddac3
--- a/src/ZF/Univ.thy	Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Univ.thy	Tue Jun 21 17:20:34 1994 +0200
@@ -10,18 +10,15 @@
 
 Univ = Arith + Sum + "mono" +
 consts
-    Limit       ::      "i=>o"
-    Vfrom       ::      "[i,i]=>i"
-    Vset        ::      "i=>i"
-    Vrec        ::      "[i, [i,i]=>i] =>i"
-    univ        ::      "i=>i"
+    Vfrom       :: "[i,i]=>i"
+    Vset        :: "i=>i"
+    Vrec        :: "[i, [i,i]=>i] =>i"
+    univ        :: "i=>i"
 
 translations
     "Vset(x)"   == 	"Vfrom(0,x)"
 
 rules
-    Limit_def   "Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
-
     Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
 
     Vrec_def