src/HOL/Fun.ML
changeset 1561 9ba6d69f7763
parent 1465 5d7a7e439cec
child 1666 5183de4c496d
equal deleted inserted replaced
1560:9d001e5f43d8 1561:9ba6d69f7763
   175 val set_cs = HOL_cs 
   175 val set_cs = HOL_cs 
   176     addSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI, 
   176     addSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI, 
   177             ComplI, IntI, DiffI, UnCI, insertCI] 
   177             ComplI, IntI, DiffI, UnCI, insertCI] 
   178     addIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI] 
   178     addIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI] 
   179     addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
   179     addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
       
   180 	    make_elim singleton_inject,
   180             CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE] 
   181             CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE] 
   181     addEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
   182     addEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
   182             subsetD, subsetCE];
   183             subsetD, subsetCE];
   183 
   184 
   184 fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs;
   185 fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs;