src/ZF/QUniv.thy
changeset 753 ec86863e87c8
parent 124 858ab9a9b047
child 1401 0c439768f45c
     1.1 --- a/src/ZF/QUniv.thy	Mon Nov 28 19:48:30 1994 +0100
     1.2 +++ b/src/ZF/QUniv.thy	Tue Nov 29 00:31:31 1994 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  consts
     1.5      quniv        :: "i=>i"
     1.6  
     1.7 -rules
     1.8 +defs
     1.9      quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
    1.10  
    1.11  end