diff -r 4f169d2cf6f3 -r 782f0b662cae src/Doc/Implementation/Eq.thy
--- a/src/Doc/Implementation/Eq.thy	Tue Oct 07 21:28:24 2014 +0200
+++ b/src/Doc/Implementation/Eq.thy	Tue Oct 07 21:29:59 2014 +0200
@@ -2,9 +2,9 @@
 imports Base
 begin
 
-chapter {* Equational reasoning *}
+chapter \<open>Equational reasoning\<close>
 
-text {* Equality is one of the most fundamental concepts of
+text \<open>Equality is one of the most fundamental concepts of
   mathematics.  The Isabelle/Pure logic (\chref{ch:logic}) provides a
   builtin relation @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} that expresses equality
   of arbitrary terms (or propositions) at the framework level, as
@@ -26,12 +26,12 @@
   equivalence, and relate it with the Pure equality.  This enables to
   re-use the Pure tools for equational reasoning for particular
   object-logic connectives as well.
-*}
+\<close>
 
 
-section {* Basic equality rules \label{sec:eq-rules} *}
+section \<open>Basic equality rules \label{sec:eq-rules}\<close>
 
-text {* Isabelle/Pure uses @{text "\<equiv>"} for equality of arbitrary
+text \<open>Isabelle/Pure uses @{text "\<equiv>"} for equality of arbitrary
   terms, which includes equivalence of propositions of the logical
   framework.  The conceptual axiomatization of the constant @{text "\<equiv>
   :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} is given in \figref{fig:pure-equality}.  The
@@ -50,9 +50,9 @@
   inference function, although the rule attribute @{attribute THEN} or
   ML operator @{ML "op RS"} involve the full machinery of higher-order
   unification (modulo @{text "\<beta>\<eta>"}-conversion) and lifting of @{text
-  "\<And>/\<Longrightarrow>"} contexts. *}
+  "\<And>/\<Longrightarrow>"} contexts.\<close>
 
-text %mlref {*
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML Thm.reflexive: "cterm -> thm"} \\
   @{index_ML Thm.symmetric: "thm -> thm"} \\
@@ -67,29 +67,29 @@
   these inference rules, and a few more for primitive @{text "\<beta>"} and
   @{text "\<eta>"} conversions.  Note that @{text "\<alpha>"} conversion is
   implicit due to the representation of terms with de-Bruijn indices
-  (\secref{sec:terms}). *}
+  (\secref{sec:terms}).\<close>
 
 
-section {* Conversions \label{sec:conv} *}
+section \<open>Conversions \label{sec:conv}\<close>
 
-text {*
+text \<open>
   %FIXME
 
   The classic article that introduces the concept of conversion (for
   Cambridge LCF) is @{cite "paulson:1983"}.
-*}
+\<close>
 
 
-section {* Rewriting \label{sec:rewriting} *}
+section \<open>Rewriting \label{sec:rewriting}\<close>
 
-text {* Rewriting normalizes a given term (theorem or goal) by
+text \<open>Rewriting normalizes a given term (theorem or goal) by
   replacing instances of given equalities @{text "t \<equiv> u"} in subterms.
   Rewriting continues until no rewrites are applicable to any subterm.
   This may be used to unfold simple definitions of the form @{text "f
   x\<^sub>1 \<dots> x\<^sub>n \<equiv> u"}, but is slightly more general than that.
-*}
+\<close>
 
-text %mlref {*
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\
   @{index_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\
@@ -121,6 +121,6 @@
   in the proof state.
 
   \end{description}
-*}
+\<close>
 
 end