diff -r fb7756087101 -r 38b049cd3aad src/Doc/Implementation/Eq.thy
--- a/src/Doc/Implementation/Eq.thy	Wed Dec 16 16:31:36 2015 +0100
+++ b/src/Doc/Implementation/Eq.thy	Wed Dec 16 17:28:49 2015 +0100
@@ -6,52 +6,52 @@
 
 chapter \<open>Equational reasoning\<close>
 
-text \<open>Equality is one of the most fundamental concepts of
-  mathematics.  The Isabelle/Pure logic (\chref{ch:logic}) provides a
-  builtin relation \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> that expresses equality
-  of arbitrary terms (or propositions) at the framework level, as
-  expressed by certain basic inference rules (\secref{sec:eq-rules}).
+text \<open>
+  Equality is one of the most fundamental concepts of mathematics. The
+  Isabelle/Pure logic (\chref{ch:logic}) provides a builtin relation \<open>\<equiv> :: \<alpha> \<Rightarrow>
+  \<alpha> \<Rightarrow> prop\<close> that expresses equality of arbitrary terms (or propositions) at
+  the framework level, as expressed by certain basic inference rules
+  (\secref{sec:eq-rules}).
 
-  Equational reasoning means to replace equals by equals, using
-  reflexivity and transitivity to form chains of replacement steps,
-  and congruence rules to access sub-structures.  Conversions
-  (\secref{sec:conv}) provide a convenient framework to compose basic
-  equational steps to build specific equational reasoning tools.
+  Equational reasoning means to replace equals by equals, using reflexivity
+  and transitivity to form chains of replacement steps, and congruence rules
+  to access sub-structures. Conversions (\secref{sec:conv}) provide a
+  convenient framework to compose basic equational steps to build specific
+  equational reasoning tools.
 
-  Higher-order matching is able to provide suitable instantiations for
-  giving equality rules, which leads to the versatile concept of
-  \<open>\<lambda>\<close>-term rewriting (\secref{sec:rewriting}).  Internally
-  this is based on the general-purpose Simplifier engine of Isabelle,
-  which is more specific and more efficient than plain conversions.
+  Higher-order matching is able to provide suitable instantiations for giving
+  equality rules, which leads to the versatile concept of \<open>\<lambda>\<close>-term rewriting
+  (\secref{sec:rewriting}). Internally this is based on the general-purpose
+  Simplifier engine of Isabelle, which is more specific and more efficient
+  than plain conversions.
 
-  Object-logics usually introduce specific notions of equality or
-  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.
+  Object-logics usually introduce specific notions of equality or 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 \<open>Basic equality rules \label{sec:eq-rules}\<close>
 
-text \<open>Isabelle/Pure uses \<open>\<equiv>\<close> for equality of arbitrary
-  terms, which includes equivalence of propositions of the logical
-  framework.  The conceptual axiomatization of the constant \<open>\<equiv>
-  :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> is given in \figref{fig:pure-equality}.  The
-  inference kernel presents slightly different equality rules, which
-  may be understood as derived rules from this minimal axiomatization.
-  The Pure theory also provides some theorems that express the same
-  reasoning schemes as theorems that can be composed like object-level
+text \<open>
+  Isabelle/Pure uses \<open>\<equiv>\<close> for equality of arbitrary terms, which includes
+  equivalence of propositions of the logical framework. The conceptual
+  axiomatization of the constant \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> is given in
+  \figref{fig:pure-equality}. The inference kernel presents slightly different
+  equality rules, which may be understood as derived rules from this minimal
+  axiomatization. The Pure theory also provides some theorems that express the
+  same reasoning schemes as theorems that can be composed like object-level
   rules as explained in \secref{sec:obj-rules}.
 
-  For example, @{ML Thm.symmetric} as Pure inference is an ML function
-  that maps a theorem \<open>th\<close> stating \<open>t \<equiv> u\<close> to one
-  stating \<open>u \<equiv> t\<close>.  In contrast, @{thm [source]
-  Pure.symmetric} as Pure theorem expresses the same reasoning in
-  declarative form.  If used like \<open>th [THEN Pure.symmetric]\<close>
-  in Isar source notation, it achieves a similar effect as the ML
-  inference function, although the rule attribute @{attribute THEN} or
-  ML operator @{ML "op RS"} involve the full machinery of higher-order
-  unification (modulo \<open>\<beta>\<eta>\<close>-conversion) and lifting of \<open>\<And>/\<Longrightarrow>\<close> contexts.\<close>
+  For example, @{ML Thm.symmetric} as Pure inference is an ML function that
+  maps a theorem \<open>th\<close> stating \<open>t \<equiv> u\<close> to one stating \<open>u \<equiv> t\<close>. In contrast,
+  @{thm [source] Pure.symmetric} as Pure theorem expresses the same reasoning
+  in declarative form. If used like \<open>th [THEN Pure.symmetric]\<close> in Isar source
+  notation, it achieves a similar effect as the ML inference function,
+  although the rule attribute @{attribute THEN} or ML operator @{ML "op RS"}
+  involve the full machinery of higher-order unification (modulo
+  \<open>\<beta>\<eta>\<close>-conversion) and lifting of \<open>\<And>/\<Longrightarrow>\<close> contexts.
+\<close>
 
 text %mlref \<open>
   \begin{mldecls}
@@ -64,11 +64,11 @@
   @{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}).\<close>
+  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}).
+\<close>
 
 
 section \<open>Conversions \label{sec:conv}\<close>
@@ -76,19 +76,19 @@
 text \<open>
   %FIXME
 
-  The classic article that introduces the concept of conversion (for
-  Cambridge LCF) is @{cite "paulson:1983"}.
+  The classic article that introduces the concept of conversion (for Cambridge
+  LCF) is @{cite "paulson:1983"}.
 \<close>
 
 
 section \<open>Rewriting \label{sec:rewriting}\<close>
 
-text \<open>Rewriting normalizes a given term (theorem or goal) by
-  replacing instances of given equalities \<open>t \<equiv> u\<close> in subterms.
-  Rewriting continues until no rewrites are applicable to any subterm.
-  This may be used to unfold simple definitions of the form \<open>f
-  x\<^sub>1 \<dots> x\<^sub>n \<equiv> u\<close>, but is slightly more general than that.
-\<close>
+text \<open>
+  Rewriting normalizes a given term (theorem or goal) by replacing instances
+  of given equalities \<open>t \<equiv> u\<close> in subterms. Rewriting continues until no
+  rewrites are applicable to any subterm. This may be used to unfold simple
+  definitions of the form \<open>f x\<^sub>1 \<dots> x\<^sub>n \<equiv> u\<close>, but is slightly more general than
+  that. \<close>
 
 text %mlref \<open>
   \begin{mldecls}
@@ -99,24 +99,24 @@
   @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
   \end{mldecls}
 
-  \<^descr> @{ML rewrite_rule}~\<open>ctxt rules thm\<close> rewrites the whole
-  theorem by the given rules.
+  \<^descr> @{ML rewrite_rule}~\<open>ctxt rules thm\<close> rewrites the whole theorem by the
+  given rules.
 
-  \<^descr> @{ML rewrite_goals_rule}~\<open>ctxt rules thm\<close> rewrites the
-  outer premises of the given theorem.  Interpreting the same as a
-  goal state (\secref{sec:tactical-goals}) it means to rewrite all
-  subgoals (in the same manner as @{ML rewrite_goals_tac}).
+  \<^descr> @{ML rewrite_goals_rule}~\<open>ctxt rules thm\<close> rewrites the outer premises of
+  the given theorem. Interpreting the same as a goal state
+  (\secref{sec:tactical-goals}) it means to rewrite all subgoals (in the same
+  manner as @{ML rewrite_goals_tac}).
 
-  \<^descr> @{ML rewrite_goal_tac}~\<open>ctxt rules i\<close> rewrites subgoal
-  \<open>i\<close> by the given rewrite rules.
+  \<^descr> @{ML rewrite_goal_tac}~\<open>ctxt rules i\<close> rewrites subgoal \<open>i\<close> by the given
+  rewrite rules.
 
-  \<^descr> @{ML rewrite_goals_tac}~\<open>ctxt rules\<close> rewrites all subgoals
-  by the given rewrite rules.
+  \<^descr> @{ML rewrite_goals_tac}~\<open>ctxt rules\<close> rewrites all subgoals by the given
+  rewrite rules.
 
-  \<^descr> @{ML fold_goals_tac}~\<open>ctxt rules\<close> essentially uses @{ML
-  rewrite_goals_tac} with the symmetric form of each member of \<open>rules\<close>, re-ordered to fold longer expression first.  This supports
-  to idea to fold primitive definitions that appear in expended form
-  in the proof state.
+  \<^descr> @{ML fold_goals_tac}~\<open>ctxt rules\<close> essentially uses @{ML rewrite_goals_tac}
+  with the symmetric form of each member of \<open>rules\<close>, re-ordered to fold longer
+  expression first. This supports to idea to fold primitive definitions that
+  appear in expended form in the proof state.
 \<close>
 
 end