--- a/Fun.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/Fun.ML Thu Aug 25 11:01:45 1994 +0200
@@ -167,10 +167,10 @@
(*** Set reasoning tools ***)
val set_cs = HOL_cs
- addSIs [ballI, subsetI, InterI, INT_I, INT1_I, CollectI,
+ addSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI,
ComplI, IntI, DiffI, UnCI, insertCI]
addIs [bexI, UnionI, UN_I, UN1_I, imageI, rangeI]
- addSEs [bexE, UnionE, UN_E, UN1_E, DiffE,
+ addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE]
addEs [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
subsetD, subsetCE];