diff -r fb7756087101 -r 38b049cd3aad src/Doc/Implementation/Local_Theory.thy
--- a/src/Doc/Implementation/Local_Theory.thy	Wed Dec 16 16:31:36 2015 +0100
+++ b/src/Doc/Implementation/Local_Theory.thy	Wed Dec 16 17:28:49 2015 +0100
@@ -7,49 +7,45 @@
 chapter \<open>Local theory specifications \label{ch:local-theory}\<close>
 
 text \<open>
-  A \<^emph>\<open>local theory\<close> combines aspects of both theory and proof
-  context (cf.\ \secref{sec:context}), such that definitional
-  specifications may be given relatively to parameters and
-  assumptions.  A local theory is represented as a regular proof
-  context, augmented by administrative data about the \<^emph>\<open>target
+  A \<^emph>\<open>local theory\<close> combines aspects of both theory and proof context (cf.\
+  \secref{sec:context}), such that definitional specifications may be given
+  relatively to parameters and assumptions. A local theory is represented as a
+  regular proof context, augmented by administrative data about the \<^emph>\<open>target
   context\<close>.
 
-  The target is usually derived from the background theory by adding
-  local \<open>\<FIX>\<close> and \<open>\<ASSUME>\<close> elements, plus
-  suitable modifications of non-logical context data (e.g.\ a special
-  type-checking discipline).  Once initialized, the target is ready to
-  absorb definitional primitives: \<open>\<DEFINE>\<close> for terms and
-  \<open>\<NOTE>\<close> for theorems.  Such definitions may get
-  transformed in a target-specific way, but the programming interface
-  hides such details.
+  The target is usually derived from the background theory by adding local
+  \<open>\<FIX>\<close> and \<open>\<ASSUME>\<close> elements, plus suitable modifications of
+  non-logical context data (e.g.\ a special type-checking discipline). Once
+  initialized, the target is ready to absorb definitional primitives:
+  \<open>\<DEFINE>\<close> for terms and \<open>\<NOTE>\<close> for theorems. Such definitions may get
+  transformed in a target-specific way, but the programming interface hides
+  such details.
 
   Isabelle/Pure provides target mechanisms for locales, type-classes,
-  type-class instantiations, and general overloading.  In principle,
-  users can implement new targets as well, but this rather arcane
-  discipline is beyond the scope of this manual.  In contrast,
-  implementing derived definitional packages to be used within a local
-  theory context is quite easy: the interfaces are even simpler and
-  more abstract than the underlying primitives for raw theories.
+  type-class instantiations, and general overloading. In principle, users can
+  implement new targets as well, but this rather arcane discipline is beyond
+  the scope of this manual. In contrast, implementing derived definitional
+  packages to be used within a local theory context is quite easy: the
+  interfaces are even simpler and more abstract than the underlying primitives
+  for raw theories.
 
-  Many definitional packages for local theories are available in
-  Isabelle.  Although a few old packages only work for global
-  theories, the standard way of implementing definitional packages in
-  Isabelle is via the local theory interface.
+  Many definitional packages for local theories are available in Isabelle.
+  Although a few old packages only work for global theories, the standard way
+  of implementing definitional packages in Isabelle is via the local theory
+  interface.
 \<close>
 
 
 section \<open>Definitional elements\<close>
 
 text \<open>
-  There are separate elements \<open>\<DEFINE> c \<equiv> t\<close> for terms, and
-  \<open>\<NOTE> b = thm\<close> for theorems.  Types are treated
-  implicitly, according to Hindley-Milner discipline (cf.\
-  \secref{sec:variables}).  These definitional primitives essentially
-  act like \<open>let\<close>-bindings within a local context that may
-  already contain earlier \<open>let\<close>-bindings and some initial
-  \<open>\<lambda>\<close>-bindings.  Thus we gain \<^emph>\<open>dependent definitions\<close>
-  that are relative to an initial axiomatic context.  The following
-  diagram illustrates this idea of axiomatic elements versus
+  There are separate elements \<open>\<DEFINE> c \<equiv> t\<close> for terms, and \<open>\<NOTE> b =
+  thm\<close> for theorems. Types are treated implicitly, according to Hindley-Milner
+  discipline (cf.\ \secref{sec:variables}). These definitional primitives
+  essentially act like \<open>let\<close>-bindings within a local context that may already
+  contain earlier \<open>let\<close>-bindings and some initial \<open>\<lambda>\<close>-bindings. Thus we gain
+  \<^emph>\<open>dependent definitions\<close> that are relative to an initial axiomatic context.
+  The following diagram illustrates this idea of axiomatic elements versus
   definitional elements:
 
   \begin{center}
@@ -64,34 +60,33 @@
   \end{tabular}
   \end{center}
 
-  A user package merely needs to produce suitable \<open>\<DEFINE>\<close>
-  and \<open>\<NOTE>\<close> elements according to the application.  For
-  example, a package for inductive definitions might first \<open>\<DEFINE>\<close> a certain predicate as some fixed-point construction,
-  then \<open>\<NOTE>\<close> a proven result about monotonicity of the
+  A user package merely needs to produce suitable \<open>\<DEFINE>\<close> and \<open>\<NOTE>\<close>
+  elements according to the application. For example, a package for inductive
+  definitions might first \<open>\<DEFINE>\<close> a certain predicate as some fixed-point
+  construction, then \<open>\<NOTE>\<close> a proven result about monotonicity of the
   functor involved here, and then produce further derived concepts via
   additional \<open>\<DEFINE>\<close> and \<open>\<NOTE>\<close> elements.
 
-  The cumulative sequence of \<open>\<DEFINE>\<close> and \<open>\<NOTE>\<close>
-  produced at package runtime is managed by the local theory
-  infrastructure by means of an \<^emph>\<open>auxiliary context\<close>.  Thus the
-  system holds up the impression of working within a fully abstract
-  situation with hypothetical entities: \<open>\<DEFINE> c \<equiv> t\<close>
-  always results in a literal fact \<open>\<^BG>c \<equiv> t\<^EN>\<close>, where
-  \<open>c\<close> is a fixed variable \<open>c\<close>.  The details about
-  global constants, name spaces etc. are handled internally.
+  The cumulative sequence of \<open>\<DEFINE>\<close> and \<open>\<NOTE>\<close> produced at package
+  runtime is managed by the local theory infrastructure by means of an
+  \<^emph>\<open>auxiliary context\<close>. Thus the system holds up the impression of working
+  within a fully abstract situation with hypothetical entities: \<open>\<DEFINE> c \<equiv>
+  t\<close> always results in a literal fact \<open>\<^BG>c \<equiv> t\<^EN>\<close>, where \<open>c\<close> is a
+  fixed variable \<open>c\<close>. The details about global constants, name spaces etc. are
+  handled internally.
 
-  So the general structure of a local theory is a sandwich of three
-  layers:
+  So the general structure of a local theory is a sandwich of three layers:
 
   \begin{center}
   \framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}}
   \end{center}
 
-  When a definitional package is finished, the auxiliary context is
-  reset to the target context.  The target now holds definitions for
-  terms and theorems that stem from the hypothetical \<open>\<DEFINE>\<close> and \<open>\<NOTE>\<close> elements, transformed by the
-  particular target policy (see @{cite \<open>\S4--5\<close> "Haftmann-Wenzel:2009"}
-  for details).\<close>
+  When a definitional package is finished, the auxiliary context is reset to
+  the target context. The target now holds definitions for terms and theorems
+  that stem from the hypothetical \<open>\<DEFINE>\<close> and \<open>\<NOTE>\<close> elements,
+  transformed by the particular target policy (see @{cite \<open>\S4--5\<close>
+  "Haftmann-Wenzel:2009"} for details).
+\<close>
 
 text %mlref \<open>
   \begin{mldecls}
@@ -103,50 +98,45 @@
     local_theory -> (string * thm list) * local_theory"} \\
   \end{mldecls}
 
-  \<^descr> Type @{ML_type local_theory} represents local theories.
-  Although this is merely an alias for @{ML_type Proof.context}, it is
-  semantically a subtype of the same: a @{ML_type local_theory} holds
-  target information as special context data.  Subtyping means that
-  any value \<open>lthy:\<close>~@{ML_type local_theory} can be also used
-  with operations on expecting a regular \<open>ctxt:\<close>~@{ML_type
+  \<^descr> Type @{ML_type local_theory} represents local theories. Although this is
+  merely an alias for @{ML_type Proof.context}, it is semantically a subtype
+  of the same: a @{ML_type local_theory} holds target information as special
+  context data. Subtyping means that any value \<open>lthy:\<close>~@{ML_type local_theory}
+  can be also used with operations on expecting a regular \<open>ctxt:\<close>~@{ML_type
   Proof.context}.
 
-  \<^descr> @{ML Named_Target.init}~\<open>before_exit name thy\<close>
-  initializes a local theory derived from the given background theory.
-  An empty name refers to a \<^emph>\<open>global theory\<close> context, and a
-  non-empty name refers to a @{command locale} or @{command class}
-  context (a fully-qualified internal name is expected here).  This is
-  useful for experimentation --- normally the Isar toplevel already
+  \<^descr> @{ML Named_Target.init}~\<open>before_exit name thy\<close> initializes a local theory
+  derived from the given background theory. An empty name refers to a \<^emph>\<open>global
+  theory\<close> context, and a non-empty name refers to a @{command locale} or
+  @{command class} context (a fully-qualified internal name is expected here).
+  This is useful for experimentation --- normally the Isar toplevel already
   takes care to initialize the local theory context.
 
-  \<^descr> @{ML Local_Theory.define}~\<open>((b, mx), (a, rhs))
-  lthy\<close> defines a local entity according to the specification that is
-  given relatively to the current \<open>lthy\<close> context.  In
-  particular the term of the RHS may refer to earlier local entities
-  from the auxiliary context, or hypothetical parameters from the
-  target context.  The result is the newly defined term (which is
-  always a fixed variable with exactly the same name as specified for
-  the LHS), together with an equational theorem that states the
-  definition as a hypothetical fact.
+  \<^descr> @{ML Local_Theory.define}~\<open>((b, mx), (a, rhs)) lthy\<close> defines a local
+  entity according to the specification that is given relatively to the
+  current \<open>lthy\<close> context. In particular the term of the RHS may refer to
+  earlier local entities from the auxiliary context, or hypothetical
+  parameters from the target context. The result is the newly defined term
+  (which is always a fixed variable with exactly the same name as specified
+  for the LHS), together with an equational theorem that states the definition
+  as a hypothetical fact.
 
-  Unless an explicit name binding is given for the RHS, the resulting
-  fact will be called \<open>b_def\<close>.  Any given attributes are
-  applied to that same fact --- immediately in the auxiliary context
-  \<^emph>\<open>and\<close> in any transformed versions stemming from target-specific
-  policies or any later interpretations of results from the target
-  context (think of @{command locale} and @{command interpretation},
-  for example).  This means that attributes should be usually plain
-  declarations such as @{attribute simp}, while non-trivial rules like
+  Unless an explicit name binding is given for the RHS, the resulting fact
+  will be called \<open>b_def\<close>. Any given attributes are applied to that same fact
+  --- immediately in the auxiliary context \<^emph>\<open>and\<close> in any transformed versions
+  stemming from target-specific policies or any later interpretations of
+  results from the target context (think of @{command locale} and @{command
+  interpretation}, for example). This means that attributes should be usually
+  plain declarations such as @{attribute simp}, while non-trivial rules like
   @{attribute simplified} are better avoided.
 
-  \<^descr> @{ML Local_Theory.note}~\<open>(a, ths) lthy\<close> is
-  analogous to @{ML Local_Theory.define}, but defines facts instead of
-  terms.  There is also a slightly more general variant @{ML
-  Local_Theory.notes} that defines several facts (with attribute
-  expressions) simultaneously.
+  \<^descr> @{ML Local_Theory.note}~\<open>(a, ths) lthy\<close> is analogous to @{ML
+  Local_Theory.define}, but defines facts instead of terms. There is also a
+  slightly more general variant @{ML Local_Theory.notes} that defines several
+  facts (with attribute expressions) simultaneously.
 
-  This is essentially the internal version of the @{command lemmas}
-  command, or @{command declare} if an empty name binding is given.
+  This is essentially the internal version of the @{command lemmas} command,
+  or @{command declare} if an empty name binding is given.
 \<close>