src/HOL/Decision_Procs/mir_tac.ML
changeset 29948 cdf12a1cb963
parent 29823 0ab754d13ccd
child 30031 bd786c37af84
child 30240 5b25fee0362c
     1.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Mon Feb 16 19:35:52 2009 -0800
     1.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Tue Feb 17 18:48:17 2009 +0100
     1.3 @@ -49,7 +49,7 @@
     1.4  val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym;
     1.5  val nat_mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
     1.6  val nat_mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
     1.7 -val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;
     1.8 +val int_mod_add_eq = @{thm "mod_add_eq"} RS sym;
     1.9  val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
    1.10  val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
    1.11  val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;