Now set_cs is just taken from !claset
authorpaulson
Fri, 28 Jun 1996 11:16:12 +0200
changeset 1837 ce5dc74dec97
parent 1836 861e29c7cada
child 1838 91e0395adc72
Now set_cs is just taken from !claset
src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Jun 28 11:13:07 1996 +0200
+++ b/src/HOL/Fun.ML	Fri Jun 28 11:16:12 1996 +0200
@@ -179,14 +179,6 @@
 AddEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
             subsetD, subsetCE];
 
-val set_cs = HOL_cs 
-    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, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
-            make_elim singleton_inject,
-            CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE] 
-    addEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
-            subsetD, subsetCE];
+val set_cs = !claset delrules [equalityI];
 
 fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac (claset_of "Fun");