src/ZF/Univ.thy
changeset 516 1957113f0d7d
parent 490 e6f0214ddac3
child 753 ec86863e87c8
equal deleted inserted replaced
515:abcc438e7c27 516:1957113f0d7d
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 The cumulative hierarchy and a small universe for recursive types
     6 The cumulative hierarchy and a small universe for recursive types
     7 
     7 
     8 Standard notation for Vset(i) is V(i), but users might want V for a variable
     8 Standard notation for Vset(i) is V(i), but users might want V for a variable
       
     9 
       
    10 NOTE: univ(A) could be a translation; would simplify many proofs!
       
    11   But Ind_Syntax.univ refers to the constant "univ"
     9 *)
    12 *)
    10 
    13 
    11 Univ = Arith + Sum + Fin + "mono" +
    14 Univ = Arith + Sum + "mono" +
    12 consts
    15 consts
    13     Vfrom       :: "[i,i]=>i"
    16     Vfrom       :: "[i,i]=>i"
    14     Vset        :: "i=>i"
    17     Vset        :: "i=>i"
    15     Vrec        :: "[i, [i,i]=>i] =>i"
    18     Vrec        :: "[i, [i,i]=>i] =>i"
    16     univ        :: "i=>i"
    19     univ        :: "i=>i"