src/ZF/Univ.thy
changeset 3923 c257b82a1200
parent 2469 b50b8c0eec01
child 3940 1d5bee4d047f
equal deleted inserted replaced
3922:ca23ee574faa 3923:c257b82a1200
    10 NOTE: univ(A) could be a translation; would simplify many proofs!
    10 NOTE: univ(A) could be a translation; would simplify many proofs!
    11   But Ind_Syntax.univ refers to the constant "univ"
    11   But Ind_Syntax.univ refers to the constant "univ"
    12 *)
    12 *)
    13 
    13 
    14 Univ = Arith + Sum + Finite + mono +
    14 Univ = Arith + Sum + Finite + mono +
       
    15 
       
    16 global
       
    17 
    15 consts
    18 consts
    16     Vfrom       :: [i,i]=>i
    19     Vfrom       :: [i,i]=>i
    17     Vset        :: i=>i
    20     Vset        :: i=>i
    18     Vrec        :: [i, [i,i]=>i] =>i
    21     Vrec        :: [i, [i,i]=>i] =>i
    19     univ        :: i=>i
    22     univ        :: i=>i
    20 
    23 
    21 translations
    24 translations
    22     "Vset(x)"   ==      "Vfrom(0,x)"
    25     "Vset(x)"   ==      "Vfrom(0,x)"
       
    26 
       
    27 path Univ
    23 
    28 
    24 defs
    29 defs
    25     Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
    30     Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
    26 
    31 
    27     Vrec_def
    32     Vrec_def