# HG changeset patch
# User paulson
# Date 956482481 -7200
# Node ID 1bc30ff5fc546257d46962f878fbaa3dc4147baf
# Parent  3f976a7e81d31909cb17b731cf6ea56ae8c5c5de
[Int_CC.sum_conv, Int_CC.rel_conv] no longer exist

diff -r 3f976a7e81d3 -r 1bc30ff5fc54 src/HOL/Integ/IntDiv.ML
--- a/src/HOL/Integ/IntDiv.ML	Sun Apr 23 11:34:05 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML	Sun Apr 23 11:34:41 2000 +0200
@@ -557,8 +557,7 @@
 \     ==> 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,
@@ -603,8 +602,7 @@
 \     ==> 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,
@@ -716,8 +714,7 @@
 \     ==> 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,
@@ -817,7 +814,7 @@
 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(),
@@ -851,7 +848,6 @@
 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);
@@ -877,7 +873,7 @@
 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(),
@@ -910,7 +906,6 @@
 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);