src/ZF/Univ.thy
changeset 6093 87bf8c03b169
parent 6053 8a1059aa01f0
child 9395 1c9851cdfe9f
     1.1 --- a/src/ZF/Univ.thy	Tue Jan 12 13:54:51 1999 +0100
     1.2 +++ b/src/ZF/Univ.thy	Tue Jan 12 15:17:37 1999 +0100
     1.3 @@ -8,13 +8,11 @@
     1.4  Standard notation for Vset(i) is V(i), but users might want V for a variable
     1.5  
     1.6  NOTE: univ(A) could be a translation; would simplify many proofs!
     1.7 -  But Ind_Syntax.univ refers to the constant "univ"
     1.8 +  But Ind_Syntax.univ refers to the constant "Univ.univ"
     1.9  *)
    1.10  
    1.11  Univ = Arith + Sum + Finite + mono +
    1.12  
    1.13 -global
    1.14 -
    1.15  consts
    1.16      Vfrom       :: [i,i]=>i
    1.17      Vset        :: i=>i
    1.18 @@ -25,7 +23,6 @@
    1.19  translations
    1.20      "Vset(x)"   ==      "Vfrom(0,x)"
    1.21  
    1.22 -local
    1.23  
    1.24  defs
    1.25      Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"