src/ZF/QUniv.thy
changeset 13357 6f54e992777e
parent 13356 c9cfe1638bf2
child 13615 449a70d88b38
     1.1 --- a/src/ZF/QUniv.thy	Sun Jul 14 15:14:43 2002 +0200
     1.2 +++ b/src/ZF/QUniv.thy	Sun Jul 14 19:59:55 2002 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  header{*A Small Universe for Lazy Recursive Types*}
     1.6  
     1.7 -theory QUniv = Univ + QPair + mono + equalities:
     1.8 +theory QUniv = Univ + QPair:
     1.9  
    1.10  (*Disjoint sums as a datatype*)
    1.11  rep_datatype