# HG changeset patch
# User wenzelm
# Date 1391275358 -3600
# Node ID 3229614ca9c5c9a2a50d4c4e71d3978016582267
# Parent  7a46672934a3a0d65fce200a0f69918506dd778f
method_setup "lem";

diff -r 7a46672934a3 -r 3229614ca9c5 src/Sequents/LK.thy
--- a/src/Sequents/LK.thy	Sat Feb 01 18:17:13 2014 +0100
+++ b/src/Sequents/LK.thy	Sat Feb 01 18:22:38 2014 +0100
@@ -175,7 +175,7 @@
   assumes p1: "|- P <-> P'"
     and p2: "|- P' ==> |- Q <-> Q'"
   shows "|- (P-->Q) <-> (P'-->Q')"
-  apply (tactic {* lemma_tac @{thm p1} 1 *})
+  apply (lem p1)
   apply safe
    apply (tactic {*
      REPEAT (rtac @{thm cut} 1 THEN
@@ -188,7 +188,7 @@
   assumes p1: "|- P <-> P'"
     and p2: "|- P' ==> |- Q <-> Q'"
   shows "|- (P&Q) <-> (P'&Q')"
-  apply (tactic {* lemma_tac @{thm p1} 1 *})
+  apply (lem p1)
   apply safe
    apply (tactic {*
      REPEAT (rtac @{thm cut} 1 THEN
@@ -221,12 +221,12 @@
   done
 
 lemma if_cancel: "|- (if P then x else x) = x"
-  apply (tactic {* lemma_tac @{thm split_if} 1 *})
+  apply (lem split_if)
   apply fast
   done
 
 lemma if_eq_cancel: "|- (if x=y then y else x) = x"
-  apply (tactic {* lemma_tac @{thm split_if} 1 *})
+  apply (lem split_if)
   apply safe
   apply (rule symL)
   apply (rule basic)
diff -r 7a46672934a3 -r 3229614ca9c5 src/Sequents/LK0.thy
--- 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"