--- a/src/FOL/IFOL.thy Fri Jan 04 21:49:06 2019 +0100
+++ b/src/FOL/IFOL.thy Fri Jan 04 23:22:53 2019 +0100
@@ -149,7 +149,7 @@
apply (rule major [THEN spec])
done
-text \<open>Duplicates the quantifier; for use with @{ML eresolve_tac}.\<close>
+text \<open>Duplicates the quantifier; for use with \<^ML>\<open>eresolve_tac\<close>.\<close>
lemma all_dupE:
assumes major: \<open>\<forall>x. P(x)\<close>
and r: \<open>\<lbrakk>P(x); \<forall>x. P(x)\<rbrakk> \<Longrightarrow> R\<close>
@@ -442,7 +442,7 @@
done
text \<open>
- Useful with @{ML eresolve_tac} for proving equalities from known
+ Useful with \<^ML>\<open>eresolve_tac\<close> for proving equalities from known
equalities.
a = b
@@ -499,7 +499,7 @@
text \<open>
Roy Dyckhoff has proved that \<open>conj_impE\<close>, \<open>disj_impE\<close>, and
- \<open>imp_impE\<close> used with @{ML mp_tac} (restricted to atomic formulae) is
+ \<open>imp_impE\<close> used with \<^ML>\<open>mp_tac\<close> (restricted to atomic formulae) is
COMPLETE for intuitionistic propositional logic.
See R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
@@ -608,7 +608,7 @@
subsection \<open>Intuitionistic Reasoning\<close>
-setup \<open>Intuitionistic.method_setup @{binding iprover}\<close>
+setup \<open>Intuitionistic.method_setup \<^binding>\<open>iprover\<close>\<close>
lemma impE':
assumes 1: \<open>P \<longrightarrow> Q\<close>