# HG changeset patch
# User huffman
# Date 1181698101 -7200
# Node ID 1f3b832c90c123eede3d05df3f8231dc215b8338
# Parent  9981199bf86552c1ce6b6504d8e00630cf52dc83
thm antiquotations

diff -r 9981199bf865 -r 1f3b832c90c1 src/HOL/ex/coopertac.ML
--- a/src/HOL/ex/coopertac.ML	Wed Jun 13 00:02:06 2007 +0200
+++ b/src/HOL/ex/coopertac.ML	Wed Jun 13 03:28:21 2007 +0200
@@ -92,15 +92,15 @@
     (* Simp rules for changing (n::int) to int n *)
     val simpset1 = HOL_basic_ss
       addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
-        [int_int_eq, zle_int, zless_int, zadd_int, zmult_int]
+        [@{thm int_int_eq}, @{thm zle_int}, @{thm zless_int}, @{thm zadd_int}, @{thm zmult_int}]
       addsplits [zdiff_int_split]
     (*simp rules for elimination of int n*)
 
     val simpset2 = HOL_basic_ss
-      addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]
-      addcongs [conj_le_cong, imp_le_cong]
+      addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm number_of1}, @{thm number_of2}, @{thm int_0}, @{thm int_1}]
+      addcongs [@{thm conj_le_cong}, @{thm imp_le_cong}]
     (* simp rules for elimination of abs *)
-    val simpset3 = HOL_basic_ss addsplits [abs_split]
+    val simpset3 = HOL_basic_ss addsplits [@{thm abs_split}]
     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
     (* Theorem for the nat --> int transformation *)
     val pre_thm = Seq.hd (EVERY