--- a/src/CCL/CCL.thy Wed Jun 11 11:20:10 2008 +0200
+++ b/src/CCL/CCL.thy Wed Jun 11 15:40:20 2008 +0200
@@ -414,8 +414,7 @@
done
ML {*
- local val po_coinduct = thm "po_coinduct"
- in fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i end
+ fun po_coinduct_tac s i = res_inst_tac [("R",s)] @{thm po_coinduct} i
*}
@@ -460,13 +459,8 @@
done
ML {*
- local
- val eq_coinduct = thm "eq_coinduct"
- val eq_coinduct3 = thm "eq_coinduct3"
- in
- fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i
- fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i
- end
+ fun eq_coinduct_tac s i = res_inst_tac [("R",s)] @{thm eq_coinduct} i
+ fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm eq_coinduct3} i
*}
--- a/src/CCL/Hered.thy Wed Jun 11 11:20:10 2008 +0200
+++ b/src/CCL/Hered.thy Wed Jun 11 15:40:20 2008 +0200
@@ -97,8 +97,7 @@
done
ML {*
- local val HTT_coinduct = thm "HTT_coinduct"
- in fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] HTT_coinduct i end
+ fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] @{thm HTT_coinduct} i
*}
lemma HTT_coinduct3:
@@ -108,17 +107,12 @@
done
ML {*
-local
- val HTT_coinduct3 = thm "HTT_coinduct3"
- val HTTgen_def = thm "HTTgen_def"
-in
+val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
-val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3
-
-fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i
+fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm HTT_coinduct3} i
val HTTgenIs =
- map (mk_genIs (the_context ()) (thms "data_defs") (thm "HTTgenXH") (thm "HTTgen_mono"))
+ map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
["true : HTTgen(R)",
"false : HTTgen(R)",
"[| a : R; b : R |] ==> <a,b> : HTTgen(R)",
@@ -130,8 +124,6 @@
"n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
"[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
"[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==> h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"]
-
-end
*}
ML {* bind_thms ("HTTgenIs", HTTgenIs) *}
--- a/src/CCL/Wfd.thy Wed Jun 11 11:20:10 2008 +0200
+++ b/src/CCL/Wfd.thy Wed Jun 11 15:40:20 2008 +0200
@@ -54,10 +54,8 @@
done
ML {*
- local val wfd_strengthen_lemma = thm "wfd_strengthen_lemma" in
fun wfd_strengthen_tac s i =
- res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN assume_tac (i+1)
- end
+ res_inst_tac [("Q",s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
*}
lemma wf_anti_sym: "[| Wfd(r); <a,x>:r; <x,a>:r |] ==> P"
--- a/src/Sequents/LK0.thy Wed Jun 11 11:20:10 2008 +0200
+++ b/src/Sequents/LK0.thy Wed Jun 11 15:40:20 2008 +0200
@@ -155,21 +155,13 @@
by (rule exchLS)
ML {*
-local
- val thinR = thm "thinR"
- val thinL = thm "thinL"
- val cut = thm "cut"
-in
-
(*Cut and thin, replacing the right-side formula*)
fun cutR_tac s i =
- res_inst_tac [ ("P", s) ] cut i THEN rtac thinR i
+ res_inst_tac [ ("P", s) ] @{thm cut} i THEN rtac @{thm thinR} i
(*Cut and thin, replacing the left-side formula*)
fun cutL_tac s i =
- res_inst_tac [("P", s)] cut i THEN rtac thinL (i+1)
-
-end
+ res_inst_tac [("P", s)] @{thm cut} i THEN rtac @{thm thinL} (i+1)
*}