src/HOL/ex/coopertac.ML
changeset 23469 3f309f885d0b
parent 23364 1f3b832c90c1
child 23590 ad95084a5c63
     1.1 --- a/src/HOL/ex/coopertac.ML	Thu Jun 21 22:30:58 2007 +0200
     1.2 +++ b/src/HOL/ex/coopertac.ML	Thu Jun 21 22:52:22 2007 +0200
     1.3 @@ -24,9 +24,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 = mod_add1_eq RS sym;
     1.8 -val nat_mod_add_left_eq = mod_add_left_eq RS sym;
     1.9 -val nat_mod_add_right_eq = mod_add_right_eq RS sym;
    1.10 +val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
    1.11 +val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
    1.12 +val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    1.13  val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;
    1.14  val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
    1.15  val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
    1.16 @@ -77,8 +77,8 @@
    1.17  				  nat_mod_add_right_eq, int_mod_add_eq, 
    1.18  				  int_mod_add_right_eq, int_mod_add_left_eq,
    1.19  				  nat_div_add_eq, int_div_add_eq,
    1.20 -				  mod_self, @{thm "zmod_self"},
    1.21 -				  DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
    1.22 +				  @{thm mod_self}, @{thm "zmod_self"},
    1.23 +				  @{thm DIVISION_BY_ZERO_MOD}, @{thm DIVISION_BY_ZERO_DIV},
    1.24  				  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
    1.25  				  @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
    1.26  				  @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},