src/ZF/QUniv.thy
changeset 1401 0c439768f45c
parent 753 ec86863e87c8
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/QUniv.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/QUniv.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  QUniv = Univ + QPair + "mono" + "equalities" +
     1.6  consts
     1.7 -    quniv        :: "i=>i"
     1.8 +    quniv        :: i=>i
     1.9  
    1.10  defs
    1.11      quniv_def    "quniv(A) == Pow(univ(eclose(A)))"