src/ZF/QUniv.thy

--- a/src/ZF/QUniv.thy	Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/QUniv.thy	Sun Jul 14 19:59:55 2002 +0200
@@ -7,7 +7,7 @@
 
 header{*A Small Universe for Lazy Recursive Types*}
 
-theory QUniv = Univ + QPair + mono + equalities:
+theory QUniv = Univ + QPair:
 
 (*Disjoint sums as a datatype*)
 rep_datatype