| changeset 484 | 70b789956bd3 |
| parent 14 | 1c0926788772 |
| child 647 | fb7345cccddc |
--- a/src/ZF/Fixedpt.ML Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/Fixedpt.ML Tue Jul 26 13:21:20 1994 +0200 @@ -74,7 +74,7 @@ val subset0_cs = FOL_cs addSIs [ballI, InterI, CollectI, PowI, empty_subsetI] addIs [bexI, UnionI, ReplaceI, RepFunI] - addSEs [bexE, make_elim PowD, UnionE, ReplaceE, RepFunE, + addSEs [bexE, make_elim PowD, UnionE, ReplaceE2, RepFunE, CollectE, emptyE] addEs [rev_ballE, InterD, make_elim InterD, subsetD];