src/ZF/Univ.thy
changeset 2469 b50b8c0eec01
parent 1478 2b8c2a7547ab
child 3923 c257b82a1200
equal deleted inserted replaced
2468:428efffe8599 2469:b50b8c0eec01
     9 
     9 
    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 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