Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Classical.thy
changeset 69597 ff784d5a5bfb
parent 69420 85b0df070afe 
--- a/src/HOL/ex/Classical.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/ex/Classical.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -428,7 +428,7 @@
 lemma "(\<forall>x y z. R(x,y) \<and> R(y,z) \<longrightarrow> R(x,z)) \<and>
        (\<forall>x. \<exists>y. R(x,y)) \<longrightarrow>
        \<not> (\<forall>x. P x = (\<forall>y. R(x,y) \<longrightarrow> \<not> P y))"
-by (tactic\<open>Meson.safe_best_meson_tac @{context} 1\<close>)
+by (tactic\<open>Meson.safe_best_meson_tac \<^context> 1\<close>)
     \<comment> \<open>In contrast, \<open>meson\<close> is SLOW: 7.6s on griffon\<close>
 
 
@@ -722,7 +722,7 @@
        (\<forall>x y. bird x \<and> snail y \<longrightarrow> \<not>eats x y) \<and>
        (\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y \<and> eats x y))
        \<longrightarrow> (\<exists>x y. animal x \<and> animal y \<and> (\<exists>z. grain z \<and> eats y z \<and> eats x y))"
-by (tactic\<open>Meson.safe_best_meson_tac @{context} 1\<close>)
+by (tactic\<open>Meson.safe_best_meson_tac \<^context> 1\<close>)
     \<comment> \<open>Nearly twice as fast as \<open>meson\<close>,
         which performs iterative deepening rather than best-first search\<close>
isabelle