src/HOL/Decision_Procs/mir_tac.ML
changeset 31790 05c92381363c
parent 31240 2c20bcd70fbe
child 32740 9dd0a2f83429
     1.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5    val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0", 
     1.6                   "add_Suc", "add_number_of_left", "mult_number_of_left", 
     1.7 -                 "Suc_eq_add_numeral_1"])@
     1.8 +                 "Suc_eq_plus1"])@
     1.9                   (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
    1.10                   @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps} 
    1.11    val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, 
    1.12 @@ -50,7 +50,6 @@
    1.13  val split_zmod = @{thm "split_zmod"};
    1.14  val mod_div_equality' = @{thm "mod_div_equality'"};
    1.15  val split_div' = @{thm "split_div'"};
    1.16 -val Suc_plus1 = @{thm "Suc_plus1"};
    1.17  val imp_le_cong = @{thm "imp_le_cong"};
    1.18  val conj_le_cong = @{thm "conj_le_cong"};
    1.19  val mod_add_eq = @{thm "mod_add_eq"} RS sym;
    1.20 @@ -104,11 +103,11 @@
    1.21                                    @{thm "mod_self"}, @{thm "zmod_self"},
    1.22                                    @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
    1.23                                    @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
    1.24 -                                  @{thm "Suc_plus1"}]
    1.25 +                                  @{thm "Suc_eq_plus1"}]
    1.26                          addsimps @{thms add_ac}
    1.27                          addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
    1.28      val simpset0 = HOL_basic_ss
    1.29 -      addsimps [mod_div_equality', Suc_plus1]
    1.30 +      addsimps [mod_div_equality', @{thm Suc_eq_plus1}]
    1.31        addsimps comp_ths
    1.32        addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}]
    1.33      (* Simp rules for changing (n::int) to int n *)