--- a/src/Sequents/LK.thy Fri Jan 04 21:49:06 2019 +0100
+++ b/src/Sequents/LK.thy Fri Jan 04 23:22:53 2019 +0100
@@ -178,10 +178,10 @@
apply (lem p1)
apply safe
apply (tactic \<open>
- REPEAT (resolve_tac @{context} @{thms cut} 1 THEN
+ REPEAT (resolve_tac \<^context> @{thms cut} 1 THEN
DEPTH_SOLVE_1
- (resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
- Cla.safe_tac @{context} 1)\<close>)
+ (resolve_tac \<^context> [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
+ Cla.safe_tac \<^context> 1)\<close>)
done
lemma conj_cong:
@@ -191,10 +191,10 @@
apply (lem p1)
apply safe
apply (tactic \<open>
- REPEAT (resolve_tac @{context} @{thms cut} 1 THEN
+ REPEAT (resolve_tac \<^context> @{thms cut} 1 THEN
DEPTH_SOLVE_1
- (resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
- Cla.safe_tac @{context} 1)\<close>)
+ (resolve_tac \<^context> [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
+ Cla.safe_tac \<^context> 1)\<close>)
done
lemma eq_sym_conv: "\<turnstile> x = y \<longleftrightarrow> y = x"