--- a/src/HOL/Meson.thy Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Meson.thy Fri Jan 04 23:22:53 2019 +0100
@@ -28,7 +28,7 @@
and not_impD: "\<not>(P\<longrightarrow>Q) \<Longrightarrow> P \<and> \<not>Q"
and iff_to_disjD: "P=Q \<Longrightarrow> (\<not>P \<or> Q) \<and> (\<not>Q \<or> P)"
and not_iffD: "\<not>(P=Q) \<Longrightarrow> (P \<or> Q) \<and> (\<not>P \<or> \<not>Q)"
- \<comment> \<open>Much more efficient than @{prop "(P \<and> \<not>Q) \<or> (Q \<and> \<not>P)"} for computing CNF\<close>
+ \<comment> \<open>Much more efficient than \<^prop>\<open>(P \<and> \<not>Q) \<or> (Q \<and> \<not>P)\<close> for computing CNF\<close>
and not_refl_disj_D: "x \<noteq> x \<or> P \<Longrightarrow> P"
by fast+
@@ -70,7 +70,7 @@
lemma make_refined_neg_rule: "\<not>P\<or>Q \<Longrightarrow> (P \<Longrightarrow> Q)"
by blast
-text\<open>@{term P} should be a literal\<close>
+text\<open>\<^term>\<open>P\<close> should be a literal\<close>
lemma make_pos_rule: "P\<or>Q \<Longrightarrow> ((P\<Longrightarrow>\<not>P) \<Longrightarrow> Q)"
by blast