src/ZF/QUniv.thy
changeset 753 ec86863e87c8
parent 124 858ab9a9b047
child 1401 0c439768f45c
equal deleted inserted replaced
752:b89462f9d5f1 753:ec86863e87c8
     8 
     8 
     9 QUniv = Univ + QPair + "mono" + "equalities" +
     9 QUniv = Univ + QPair + "mono" + "equalities" +
    10 consts
    10 consts
    11     quniv        :: "i=>i"
    11     quniv        :: "i=>i"
    12 
    12 
    13 rules
    13 defs
    14     quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
    14     quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
    15 
    15 
    16 end
    16 end