Now set_cs is just taken from !claset
authorpaulson
Fri Jun 28 11:16:12 1996 +0200 (1996-06-28)
changeset 1837ce5dc74dec97
parent 1836 861e29c7cada
child 1838 91e0395adc72
Now set_cs is just taken from !claset
src/HOL/Fun.ML
     1.1 --- a/src/HOL/Fun.ML	Fri Jun 28 11:13:07 1996 +0200
     1.2 +++ b/src/HOL/Fun.ML	Fri Jun 28 11:16:12 1996 +0200
     1.3 @@ -179,14 +179,6 @@
     1.4  AddEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
     1.5              subsetD, subsetCE];
     1.6  
     1.7 -val set_cs = HOL_cs 
     1.8 -    addSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI, 
     1.9 -            ComplI, IntI, DiffI, UnCI, insertCI] 
    1.10 -    addIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI] 
    1.11 -    addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
    1.12 -            make_elim singleton_inject,
    1.13 -            CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE] 
    1.14 -    addEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
    1.15 -            subsetD, subsetCE];
    1.16 +val set_cs = !claset delrules [equalityI];
    1.17  
    1.18  fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac (claset_of "Fun");