--- a/src/HOL/Complex/ex/linrtac.ML Thu Jun 21 22:30:58 2007 +0200
+++ b/src/HOL/Complex/ex/linrtac.ML Thu Jun 21 22:52:22 2007 +0200
@@ -34,9 +34,9 @@
val Suc_plus1 = thm "Suc_plus1";
val imp_le_cong = thm "imp_le_cong";
val conj_le_cong = thm "conj_le_cong";
-val nat_mod_add_eq = mod_add1_eq RS sym;
-val nat_mod_add_left_eq = mod_add_left_eq RS sym;
-val nat_mod_add_right_eq = mod_add_right_eq RS sym;
+val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
+val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
+val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;
val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
@@ -114,4 +114,4 @@
"decision procedure for linear real arithmetic");
-end
\ No newline at end of file
+end
--- a/src/HOL/Tools/Qelim/presburger.ML Thu Jun 21 22:30:58 2007 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML Thu Jun 21 22:52:22 2007 +0200
@@ -119,8 +119,8 @@
addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
val div_mod_ss = HOL_basic_ss addsimps simp_thms
@ map (symmetric o mk_meta_eq)
- [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, mod_add1_eq,
- mod_add_left_eq, mod_add_right_eq,
+ [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"},
+ @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
@{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"},
@{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
@ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "DIVISION_BY_ZERO_MOD"},
--- a/src/HOL/ex/coopertac.ML Thu Jun 21 22:30:58 2007 +0200
+++ b/src/HOL/ex/coopertac.ML Thu Jun 21 22:52:22 2007 +0200
@@ -24,9 +24,9 @@
val Suc_plus1 = thm "Suc_plus1";
val imp_le_cong = thm "imp_le_cong";
val conj_le_cong = thm "conj_le_cong";
-val nat_mod_add_eq = mod_add1_eq RS sym;
-val nat_mod_add_left_eq = mod_add_left_eq RS sym;
-val nat_mod_add_right_eq = mod_add_right_eq RS sym;
+val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
+val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
+val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;
val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
@@ -77,8 +77,8 @@
nat_mod_add_right_eq, int_mod_add_eq,
int_mod_add_right_eq, int_mod_add_left_eq,
nat_div_add_eq, int_div_add_eq,
- mod_self, @{thm "zmod_self"},
- DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
+ @{thm mod_self}, @{thm "zmod_self"},
+ @{thm DIVISION_BY_ZERO_MOD}, @{thm DIVISION_BY_ZERO_DIV},
ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
@{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
@{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},