src/Sequents/LK.thy

 
 lemma imp_cong:
   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
        DEPTH_SOLVE_1
          (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN

 
 lemma conj_cong:
   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
        DEPTH_SOLVE_1
          (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN

    apply (simp add: if_not_P)
   apply fast
   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)
   done