src/HOL/Decision_Procs/cooper_tac.ML
changeset 31790 05c92381363c
parent 31240 2c20bcd70fbe
child 32740 9dd0a2f83429
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  val split_zmod = @{thm split_zmod};
     1.5  val mod_div_equality' = @{thm mod_div_equality'};
     1.6  val split_div' = @{thm split_div'};
     1.7 -val Suc_plus1 = @{thm Suc_plus1};
     1.8 +val Suc_eq_plus1 = @{thm Suc_eq_plus1};
     1.9  val imp_le_cong = @{thm imp_le_cong};
    1.10  val conj_le_cong = @{thm conj_le_cong};
    1.11  val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
    1.12 @@ -81,11 +81,11 @@
    1.13  				  @{thm mod_by_0}, @{thm div_by_0},
    1.14  				  @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
    1.15  				  @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
    1.16 -				  Suc_plus1]
    1.17 +				  Suc_eq_plus1]
    1.18  			addsimps @{thms add_ac}
    1.19  			addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
    1.20      val simpset0 = HOL_basic_ss
    1.21 -      addsimps [mod_div_equality', Suc_plus1]
    1.22 +      addsimps [mod_div_equality', Suc_eq_plus1]
    1.23        addsimps comp_arith
    1.24        addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
    1.25      (* Simp rules for changing (n::int) to int n *)