src/HOL/Integ/IntDiv.ML

 
 Goal "[| quorem((b,c),(q,r));  c ~= #0 |] \
 \     ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))";
 by (auto_tac
     (claset(),
-     simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
-               addsimps split_ifs@zmult_ac@
+     simpset() addsimps split_ifs@zmult_ac@
                         [quorem_def, linorder_neq_iff, 
 			 zadd_zmult_distrib2,
 			 pos_mod_sign,pos_mod_bound,
 			 neg_mod_sign, neg_mod_bound]));
 by (ALLGOALS(rtac zmod_zdiv_equality));

 
 Goal "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c ~= #0 |] \
 \     ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))";
 by (auto_tac
     (claset(),
-     simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
-               addsimps split_ifs@zmult_ac@
+     simpset() addsimps split_ifs@zmult_ac@
                         [quorem_def, linorder_neq_iff, 
 			 zadd_zmult_distrib2,
 			 pos_mod_sign,pos_mod_bound,
 			 neg_mod_sign, neg_mod_bound]));
 by (ALLGOALS(rtac zmod_zdiv_equality));

 
 Goal "[| quorem ((a,b), (q,r));  b ~= #0;  #0 < c |] \
 \     ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
 by (auto_tac  (*SLOW*)
     (claset(),
-     simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
-               addsimps split_ifs@zmult_ac@
+     simpset() addsimps split_ifs@zmult_ac@
                         [quorem_def, linorder_neq_iff,
 			 pos_imp_zmult_pos_iff,
 			 neg_imp_zmult_pos_iff,
 			 zadd_zmult_distrib2 RS sym,
 			 lemma1, lemma2, lemma3, lemma4]));

 				  add1_zle_eq, pos_mod_bound]));
 by (stac zdiv_zadd1_eq 1);
 by (asm_simp_tac (simpset() addsimps [zdiv_zmult_zmult2, zmod_zmult_zmult2, 
 				      div_pos_pos_trivial]) 1);
 by (stac div_pos_pos_trivial 1);
-by (asm_simp_tac (simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
+by (asm_simp_tac (simpset() 
            addsimps zadd_ac@ [zmult_2_right, mod_pos_pos_trivial,
                     pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [mod_pos_pos_trivial]));
 qed "pos_zdiv_times_2";

 \          then number_of v div (number_of w)    \
 \          else (number_of v + (#1::int)) div (number_of w))";
 by (simp_tac (simpset_of Int.thy
 			 addsimps [zadd_assoc, number_of_BIT]) 1);
 by (asm_simp_tac (simpset()
-		  delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
                   delsimps bin_arith_extra_simps@bin_rel_simps
 		  addsimps [zmult_2 RS sym, zdiv_zmult_zmult1,
 			    pos_zdiv_times_2, lemma, neg_zdiv_times_2]) 1);
 qed "zdiv_number_of_BIT";
 

 				  add1_zle_eq, pos_mod_bound]));
 by (stac zmod_zadd1_eq 1);
 by (asm_simp_tac (simpset() addsimps [zmod_zmult_zmult2, 
 				      mod_pos_pos_trivial]) 1);
 by (rtac mod_pos_pos_trivial 1);
-by (asm_simp_tac (simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
+by (asm_simp_tac (simpset() 
                   addsimps zadd_ac@ [zmult_2_right, mod_pos_pos_trivial,
                     pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [mod_pos_pos_trivial]));
 qed "pos_zmod_times_2";

 \               else #2 * ((number_of v + (#1::int)) mod number_of w) - #1  \
 \          else #2 * (number_of v mod number_of w))";
 by (simp_tac (simpset_of Int.thy
 			 addsimps [zadd_assoc, number_of_BIT]) 1);
 by (asm_simp_tac (simpset()
-		  delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
 		  delsimps bin_arith_extra_simps@bin_rel_simps
 		  addsimps [zmult_2 RS sym, zmod_zmult_zmult1,
 			    pos_zmod_times_2, lemma, neg_zmod_times_2]) 1);
 qed "zmod_number_of_BIT";