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