--- a/src/FOL/IFOL.thy Mon Oct 19 23:00:07 2015 +0200
+++ b/src/FOL/IFOL.thy Mon Oct 19 23:07:17 2015 +0200
@@ -443,7 +443,7 @@
done
text \<open>
- Useful with @{ML eresolve_tac} for proving equalties from known
+ Useful with @{ML eresolve_tac} for proving equalities from known
equalities.
a = b
@@ -457,7 +457,7 @@
apply assumption+
done
-text \<open>Dual of box_equals: for proving equalities backwards.\<close>
+text \<open>Dual of @{text box_equals}: for proving equalities backwards.\<close>
lemma simp_equals: "\<lbrakk>a = c; b = d; c = d\<rbrakk> \<Longrightarrow> a = b"
apply (rule trans)
apply (rule trans)