src/ZF/Univ.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
equal deleted inserted replaced
1400:5d909faf0e04 1401:0c439768f45c
    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 consts
    15 consts
    16     Vfrom       :: "[i,i]=>i"
    16     Vfrom       :: [i,i]=>i
    17     Vset        :: "i=>i"
    17     Vset        :: i=>i
    18     Vrec        :: "[i, [i,i]=>i] =>i"
    18     Vrec        :: [i, [i,i]=>i] =>i
    19     univ        :: "i=>i"
    19     univ        :: i=>i
    20 
    20 
    21 translations
    21 translations
    22     "Vset(x)"   == 	"Vfrom(0,x)"
    22     "Vset(x)"   == 	"Vfrom(0,x)"
    23 
    23 
    24 defs
    24 defs