1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -27,12 +27,9 @@
     1.4  val Suc_plus1 = @{thm Suc_plus1};
     1.5  val imp_le_cong = @{thm imp_le_cong};
     1.6  val conj_le_cong = @{thm conj_le_cong};
     1.7 -val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
     1.8 -val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
     1.9 -val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    1.10 -val int_mod_add_eq = @{thm mod_add_eq} RS sym;
    1.11 -val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
    1.12 -val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
    1.13 +val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
    1.14 +val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    1.15 +val mod_add_eq = @{thm mod_add_eq} RS sym;
    1.16  val nat_div_add_eq = @{thm div_add1_eq} RS sym;
    1.17  val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
    1.18  
    1.19 @@ -70,14 +67,13 @@
    1.20      val (t,np,nh) = prepare_for_linz q g
    1.21      (* Some simpsets for dealing with mod div abs and nat*)
    1.22      val mod_div_simpset = HOL_basic_ss 
    1.23 -			addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, 
    1.24 -				  nat_mod_add_right_eq, int_mod_add_eq, 
    1.25 -				  int_mod_add_right_eq, int_mod_add_left_eq,
    1.26 +			addsimps [refl,mod_add_eq, mod_add_left_eq, 
    1.27 +				  mod_add_right_eq,
    1.28  				  nat_div_add_eq, int_div_add_eq,
    1.29  				  @{thm mod_self}, @{thm "zmod_self"},
    1.30  				  @{thm mod_by_0}, @{thm div_by_0},
    1.31  				  @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
    1.32 -				  @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
    1.33 +				  @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
    1.34  				  Suc_plus1]
    1.35  			addsimps @{thms add_ac}
    1.36  			addsimprocs [cancel_div_mod_proc]