--- a/src/Doc/Implementation/Eq.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Implementation/Eq.thy Fri Aug 12 17:53:55 2016 +0200
@@ -64,10 +64,10 @@
@{index_ML Thm.equal_elim: "thm -> thm -> thm"} \\
\end{mldecls}
- See also @{file "~~/src/Pure/thm.ML" } for further description of these
- inference rules, and a few more for primitive \<open>\<beta>\<close> and \<open>\<eta>\<close> conversions. Note
- that \<open>\<alpha>\<close> conversion is implicit due to the representation of terms with
- de-Bruijn indices (\secref{sec:terms}).
+ See also \<^file>\<open>~~/src/Pure/thm.ML\<close> for further description of these inference
+ rules, and a few more for primitive \<open>\<beta>\<close> and \<open>\<eta>\<close> conversions. Note that \<open>\<alpha>\<close>
+ conversion is implicit due to the representation of terms with de-Bruijn
+ indices (\secref{sec:terms}).
\<close>