src/HOL/Decision_Procs/mir_tac.ML
changeset 30224 79136ce06bdb
parent 30034 60f64f112174
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Tue Mar 03 12:14:52 2009 +1100
     1.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Tue Mar 03 17:05:18 2009 +0100
     1.3 @@ -46,10 +46,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 mod_add_eq = @{thm "mod_add_eq"} RS sym;
     1.9  val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
    1.10  val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
    1.11 -val int_mod_add_eq = @{thm "mod_add_eq"} RS sym;
    1.12  val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
    1.13  val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
    1.14  val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
    1.15 @@ -94,7 +93,7 @@
    1.16      val (t,np,nh) = prepare_for_mir thy q g
    1.17      (* Some simpsets for dealing with mod div abs and nat*)
    1.18      val mod_div_simpset = HOL_basic_ss 
    1.19 -                        addsimps [refl,nat_mod_add_eq, 
    1.20 +                        addsimps [refl, mod_add_eq, 
    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"},