src/Doc/Logics_ZF/IFOL_examples.thy
changeset 69593 3dda49e08b9d
parent 69505 cc2d676d5395
--- a/src/Doc/Logics_ZF/IFOL_examples.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/Doc/Logics_ZF/IFOL_examples.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -36,7 +36,7 @@
 done
 
 lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
-by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
 
 text\<open>Example of Dyckhoff's method\<close>
 lemma "~ ~ ((P-->Q) | (Q-->P))"