diff -r d9527f97246e -r 89669c58e506 Fun.ML
--- 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];