# HG changeset patch
# User huffman
# Date 1182459142 -7200
# Node ID 3f309f885d0ba369d41d36e16a520ffa353a1060
# Parent  d27d79a475921f11ed5c3b79cab24043ff95165f
add thm antiquotations

diff -r d27d79a47592 -r 3f309f885d0b src/HOL/Complex/ex/linrtac.ML
--- 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
diff -r d27d79a47592 -r 3f309f885d0b src/HOL/Tools/Qelim/presburger.ML
--- 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"}, 
diff -r d27d79a47592 -r 3f309f885d0b src/HOL/ex/coopertac.ML
--- 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"},