--- a/src/Sequents/LK0.thy Sat Feb 01 18:17:13 2014 +0100
+++ b/src/Sequents/LK0.thy Sat Feb 01 18:22:38 2014 +0100
@@ -232,14 +232,6 @@
|> Cla.get_pack;
*}
-ML {*
- fun lemma_tac th i =
- rtac (@{thm thinR} RS @{thm cut}) i THEN
- REPEAT (rtac @{thm thinL} i) THEN
- rtac th i;
-*}
-
-
method_setup fast_prop =
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.fast_tac (Cla.put_pack prop_pack ctxt))) *}
@@ -249,6 +241,14 @@
method_setup best_dup =
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack LK_dup_pack ctxt))) *}
+method_setup lem = {*
+ Attrib.thm >> (fn th => fn _ =>
+ SIMPLE_METHOD' (fn i =>
+ rtac (@{thm thinR} RS @{thm cut}) i THEN
+ REPEAT (rtac @{thm thinL} i) THEN
+ rtac th i))
+*}
+
lemma mp_R:
assumes major: "$H |- $E, $F, P --> Q"