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))"