src/HOL/Decision_Procs/cooper_tac.ML
changeset 30034 60f64f112174
parent 30031 bd786c37af84
child 30224 79136ce06bdb
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Feb 20 23:46:03 2009 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Feb 21 09:58:26 2009 +0100
@@ -28,11 +28,9 @@
 val imp_le_cong = @{thm imp_le_cong};
 val conj_le_cong = @{thm conj_le_cong};
 val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
-val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
-val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
+val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
+val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
 val int_mod_add_eq = @{thm mod_add_eq} RS sym;
-val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
-val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
 val nat_div_add_eq = @{thm div_add1_eq} RS sym;
 val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
 
@@ -70,9 +68,8 @@
     val (t,np,nh) = prepare_for_linz q g
     (* Some simpsets for dealing with mod div abs and nat*)
     val mod_div_simpset = HOL_basic_ss 
-			addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, 
-				  nat_mod_add_right_eq, int_mod_add_eq, 
-				  int_mod_add_right_eq, int_mod_add_left_eq,
+			addsimps [refl,nat_mod_add_eq, mod_add_left_eq, 
+				  mod_add_right_eq, int_mod_add_eq, 
 				  nat_div_add_eq, int_div_add_eq,
 				  @{thm mod_self}, @{thm "zmod_self"},
 				  @{thm mod_by_0}, @{thm div_by_0},