Improvements to the text.

--- a/doc-src/Locales/Locales/Examples.thy	Sun Mar 29 17:38:01 2009 +0200
+++ b/doc-src/Locales/Locales/Examples.thy	Tue Mar 31 21:25:08 2009 +0200
@@ -83,10 +83,12 @@
 \begin{tabular}{ll}
   \isakeyword{definition} & definition through an equation \\
   \isakeyword{inductive} & inductive definition \\
-  \isakeyword{fun}, \isakeyword{function} & recursive function \\
+  \isakeyword{primrec} & primitive recursion \\
+  \isakeyword{fun}, \isakeyword{function} & general recursion \\
   \isakeyword{abbreviation} & syntactic abbreviation \\
   \isakeyword{theorem}, etc.\ & theorem statement with proof \\
-  \isakeyword{theorems}, etc.\ & redeclaration of theorems
+  \isakeyword{theorems}, etc.\ & redeclaration of theorems \\
+  \isakeyword{text}, etc.\ & document markup
 \end{tabular}
 \end{center}
 \hrule
@@ -104,7 +106,7 @@
   locale parameter @{term le}.  Its definition is the global theorem
   @{thm [source] partial_order.less_def}:
   @{thm [display, indent=2] partial_order.less_def}
-  At the same time, the locale is extended by syntax information
+  At the same time, the locale is extended by syntax transformations
   hiding this construction in the context of the locale.  That is,
   @{term "partial_order.less le"} is printed and parsed as infix
   @{text \<sqsubset>}. *}
@@ -236,15 +238,6 @@
 
   end
 
-text {* The definitions of @{text is_inf} and @{text is_sup} look
-  like ordinary definitions in theories.  Despite, what is going on
-  behind the scenes is more complex.  The definition of @{text
-  is_inf}, say, creates a constant @{const partial_order.is_inf} where
-  the locale parameters that occur in the definition of @{text is_inf}
-  are additional arguments.  Writing @{text "is_inf x y inf"} is just
-  a notational convenience for @{text "partial_order.is_inf op \<sqsubseteq> x y
-  inf"}. *}
-
 text {* Two commands are provided to inspect locales:
   \isakeyword{print\_locales} lists the names of all locales of the
   current theory; \isakeyword{print\_locale}~$n$ prints the parameters
@@ -267,7 +260,8 @@
   distributive lattices.
 
   With locales, this inheritance is achieved through \emph{import} of a
-  locale.  The import comes before the context elements.
+  locale.  Import is a separate entity in the locale declaration.  If
+  present, it precedes the context elements.
   *}
 
   locale lattice = partial_order +
@@ -276,11 +270,8 @@
   begin
 
 text {* These assumptions refer to the predicates for infimum
-  and supremum defined in @{text partial_order}.  In the current
-  implementation of locales, syntax from definitions of the imported
-  locale is unavailable in the locale declaration, neither are their
-  names.  Hence we refer to the constants of the theory.  The names
-  and syntax is available below, in the context of the locale.  *}
+  and supremum defined in @{text partial_order}.  We may now introduce
+  the notions of meet and join.  *}
 
   definition
     meet (infixl "\<sqinter>" 70) where "x \<sqinter> y = (THE inf. is_inf x y inf)"

--- a/doc-src/Locales/Locales/Examples1.thy	Sun Mar 29 17:38:01 2009 +0200
+++ b/doc-src/Locales/Locales/Examples1.thy	Tue Mar 31 21:25:08 2009 +0200
@@ -27,7 +27,7 @@
   theories is illustrated; interpretation in proofs is analogous.
 
   As an example, consider the type of natural numbers @{typ nat}.  The
-  order relation @{text \<le>} is a total order over @{typ nat},
+  relation @{text \<le>} is a total order over @{typ nat},
   divisibility @{text dvd} is a distributive lattice.  We start with the
   interpretation that @{text \<le>} is a partial order.  The facilities of
   the interpretation command are explored in three versions.
@@ -48,7 +48,7 @@
   instantiation}.  This is a list of terms, which refer to
   the parameters in the order of declaration in the locale.  The
   locale name is preceded by an optional \emph{interpretation
-  qualifier}.
+  qualifier}, here @{text nat}.
 
   The command creates the goal%
 \footnote{Note that @{text op} binds tighter than functions
@@ -77,10 +77,6 @@
   Here, @{term "partial_order.less (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"}
   represents the strict order, although @{text "<"} is the natural
   strict order for @{typ nat}.  Interpretation allows to map concepts
-  introduced through definitions in locales to the corresponding
-  concepts of the theory.%
-\footnote{This applies not only to \isakeyword{definition} but also to
-  \isakeyword{inductive}, \isakeyword{fun} and \isakeyword{function}.} 
-  *}
-
+  introduced by definitions in locales to the corresponding
+  concepts of the theory.  *}
 end

--- a/doc-src/Locales/Locales/Examples2.thy	Sun Mar 29 17:38:01 2009 +0200
+++ b/doc-src/Locales/Locales/Examples2.thy	Tue Mar 31 21:25:08 2009 +0200
@@ -1,11 +1,10 @@
 theory Examples2
 imports Examples
 begin
-
 text {* This is achieved by unfolding suitable equations during
   interpretation.  These equations are given after the keyword
   \isakeyword{where} and require proofs.  The revised command
-  that replaces @{text "\<sqsubset>"} by @{text "<"}, is: *}
+  that replaces @{text "\<sqsubset>"} by @{text "<"} is: *}
 
 interpretation %visible nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool"
   where "partial_order.less op \<le> (x::nat) y = (x < y)"
@@ -25,5 +24,4 @@
   Hence, the correct interpretation of @{text
   "partial_order.less_def"} is obtained manually with @{text OF}.
   *}
-
 end

--- a/doc-src/Locales/Locales/Examples3.thy	Sun Mar 29 17:38:01 2009 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy	Tue Mar 31 21:25:08 2009 +0200
@@ -1,7 +1,6 @@
 theory Examples3
 imports Examples
 begin
-
 subsection {* Third Version: Local Interpretation *}
 
 text {* In the above example, the fact that @{text \<le>} is a partial
@@ -24,19 +23,15 @@
     unfolding nat.less_def by auto
 qed
 
-text {* The inner interpretation does not require an
-  elaborate new proof, it is immediate from the preceeding fact and
-  proved with ``.''.  Strict qualifiers are normally not necessary for
-  interpretations inside proofs, since these have only limited scope.
-
-  The above interpretation enriches the local proof context by
-  the very theorems also obtained in the interpretation from
-  Section~\ref{sec:po-first}, and @{text nat.less_def} may directly be
-  used to unfold the definition.  Theorems from the local
-  interpretation disappear after leaving the proof context --- that
-  is, after the closing \isakeyword{qed} --- and are
-  then replaced by those with the desired substitutions of the strict
-  order.  *}
+text {* The inner interpretation does not require an elaborate new
+  proof, it is immediate from the preceding fact and proved with
+  ``.''.  It enriches the local proof context by the very theorems
+  also obtained in the interpretation from Section~\ref{sec:po-first},
+  and @{text nat.less_def} may directly be used to unfold the
+  definition.  Theorems from the local interpretation disappear after
+  leaving the proof context --- that is, after the closing
+  \isakeyword{qed} --- and are then replaced by those with the desired
+  substitutions of the strict order.  *}
 
 
 subsection {* Further Interpretations *}
@@ -63,7 +58,7 @@
       by Presburger arithmetic. *}
     by arith+
   txt {* For the first of the equations, we refer to the theorem
-  generated in the previous interpretation. *}
+  shown in the previous interpretation. *}
   show "partial_order.less op \<le> (x::nat) y = (x < y)"
     by (rule nat_less_eq)
   txt {* In order to show the remaining equations, we put ourselves in a
@@ -75,18 +70,18 @@
     by (bestsimp simp: nat.join_def nat.is_sup_def)
 qed
 
-text {* The interpretation that the relation @{text \<le>} is a total
-  order follows next. *}
+text {* Next follows that @{text \<le>} is a total order. *}
 
 interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
   where "partial_order.less op \<le> (x::nat) y = (x < y)"
     and "lattice.meet op \<le> (x::nat) y = min x y"
     and "lattice.join op \<le> (x::nat) y = max x y"
 proof -
-  show "total_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)" by unfold_locales arith
+  show "total_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+    by unfold_locales arith
 qed (rule nat_less_eq nat_meet_eq nat_join_eq)+
 
-text {* Note that since the locale hierarchy reflects that total
+text {* Since the locale hierarchy reflects that total
   orders are distributive lattices, an explicit interpretation of
   distributive lattices for the order relation on natural numbers is
   only necessary for mapping the definitions to the right operators on
@@ -130,7 +125,8 @@
   incrementally. *}
 
 interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  where nat_dvd_less_eq: "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
+  where nat_dvd_less_eq:
+    "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
 proof -
   show "partial_order (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
     by unfold_locales (auto simp: dvd_def)
@@ -176,8 +172,8 @@
 qed
 
 text {* Equations @{thm [source] nat_dvd_meet_eq} and @{thm [source]
-  nat_dvd_join_eq} are named since they are handy in the proof of
-  the subsequent interpretation. *}
+  nat_dvd_join_eq} are used in the main part the subsequent
+  interpretation. *}
 
 (*
 definition
@@ -238,7 +234,7 @@
   *}
 
 text {*
-  The full syntax of the interpretation commands is shown in
+  The syntax of the interpretation commands is shown in
   Table~\ref{tab:commands}.  The grammar refers to
   \textit{expression}, which stands for a \emph{locale} expression.
   Locale expressions are discussed in the following section.
@@ -257,13 +253,13 @@
   Inspecting the grammar of locale commands in
   Table~\ref{tab:commands} reveals that the import of a locale can be
   more than just a single locale.  In general, the import is a
-  \emph{locale expression}.  These enable to combine locales
+  \emph{locale expression}, which enables to combine locales
   and instantiate parameters.  A locale expression is a sequence of
   locale \emph{instances} followed by an optional \isakeyword{for}
   clause.  Each instance consists of a locale reference, which may be
   preceded by a qualifer and succeeded by instantiations of the
   parameters of that locale.  Instantiations may be either positional
-  or through explicit parameter argument pairs.
+  or through explicit mappings of parameters to arguments.
 
   Using a locale expression, a locale for order
   preserving maps can be declared in the following way.  *}
@@ -275,15 +271,17 @@
     assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y"
 
 text {* The second and third line contain the expression --- two
-  instances of the partial order locale with instantiations @{text le}
+  instances of the partial order locale where the parameter is
+  instantiated to @{text le}
   and @{text le'}, respectively.  The \isakeyword{for} clause consists
   of parameter declarations and is similar to the context element
   \isakeyword{fixes}.  The notable difference is that the
   \isakeyword{for} clause is part of the expression, and only
   parameters defined in the expression may occur in its instances.
 
-  Instances are \emph{morphisms} on locales.  Their effect on the
-  parameters is naturally lifted to terms, propositions and theorems,
+  Instances define \emph{morphisms} on locales.  Their effect on the
+  parameters is lifted to terms, propositions and theorems in the
+  canonical way,
   and thus to the assumptions and conclusions of a locale.  The
   assumption of a locale expression is the conjunction of the
   assumptions of the instances.  The conclusions of a sequence of
@@ -313,22 +311,25 @@
 
 end %invisible
 
-text {* This example reveals that there is no infix syntax for the strict
-  version of @{text \<preceq>}!  This can be declared through an abbreviation.
-  *}
+text {* This example reveals that there is no infix syntax for the
+  strict operation associated with @{text \<preceq>}.  This can be declared
+  through an abbreviation.  *}
 
   abbreviation (in order_preserving)
     less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
 
 text (in order_preserving) {* Now the theorem is displayed nicely as
-  @{thm le'.less_le_trans}.  *}
+  @{thm [source]  le'.less_le_trans}:
+  @{thm [display, indent=2] le'.less_le_trans} *}
 
-text {* Qualifiers not only apply to theorem names, but also to names
-  introduced by definitions and abbreviations.  In locale
-  @{text partial_order} the full name of the strict order of @{text \<sqsubseteq>} is
-  @{text le.less} and therefore @{text le'.less} is the full name of
-  the strict order of @{text \<preceq>}.  Hence, the equation in the
-  abbreviation above could have been also written as @{text "less' \<equiv>
+text (in order_preserving)  {* Qualifiers not only apply to theorem names, but also to names
+  introduced by definitions and abbreviations.  For example, in @{text
+  partial_order} the name @{text less} abbreviates @{term
+  "partial_order.less le"}.  Therefore, in @{text order_preserving}
+  the qualified name @{text le.less} abbreviates @{term
+  "partial_order.less le"} and @{text le'.less} abbreviates @{term
+  "partial_order.less le'"}.  Hence, the equation in the abbreviation
+  above could have been written more concisely as @{text "less' \<equiv>
   le'.less"}. *}
 
 text {* Readers may find the declaration of locale @{text
@@ -342,9 +343,9 @@
   instantiation terms than the instantiated locale's number of
   parameters.  In named instantiations, instantiation pairs for
   certain parameters may simply be omitted.  Untouched parameters are
-  declared by the locale expression and with their concrete syntax by
-  implicitly adding them to the beginning of the \isakeyword{for}
-  clause.
+  implicitly declared by the locale expression and with their concrete
+  syntax.  In the sequence of parameters, they appear before the
+  parameters from the \isakeyword{for} clause.
 
   The following locales illustrate this.  A map @{text \<phi>} is a
   lattice homomorphism if it preserves meet and join. *}
@@ -352,10 +353,8 @@
   locale lattice_hom =
     le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
     fixes \<phi>
-    assumes hom_meet:
-	"\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)"
-      and hom_join:
-	"\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)"
+    assumes hom_meet: "\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)"
+      and hom_join: "\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)"
 
   abbreviation (in lattice_hom)
     meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
@@ -367,7 +366,7 @@
   locale lattice_end = lattice_hom _ le
 
 text {* In this declaration, the first parameter of @{text
-  lattice_hom}, @{text le}, is untouched and then used to instantiate
+  lattice_hom}, @{text le}, is untouched and is then used to instantiate
   the second parameter.  Its concrete syntax is preserved. *}
 
 
@@ -430,9 +429,8 @@
   Theorems and other declarations --- syntax, in particular --- from
   the locale @{text order_preserving} are now active in @{text
   lattice_hom}, for example
-
-  @{thm [source] le'.less_le_trans}:
-  @{thm le'.less_le_trans}
+  @{thm [source] hom_le}:
+  @{thm [display, indent=2] hom_le}
   *}
 
 
@@ -559,7 +557,7 @@
 \end{tabular}
 \end{center}
 \hrule
-\caption{Syntax of Locale Commands (abridged).}
+\caption{Syntax of Locale Commands.}
 \label{tab:commands}
 \end{table}
   *}

--- a/doc-src/Locales/Locales/document/Examples.tex	Sun Mar 29 17:38:01 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples.tex	Tue Mar 31 21:25:08 2009 +0200
@@ -112,10 +112,12 @@
 \begin{tabular}{ll}
   \isakeyword{definition} & definition through an equation \\
   \isakeyword{inductive} & inductive definition \\
-  \isakeyword{fun}, \isakeyword{function} & recursive function \\
+  \isakeyword{primrec} & primitive recursion \\
+  \isakeyword{fun}, \isakeyword{function} & general recursion \\
   \isakeyword{abbreviation} & syntactic abbreviation \\
   \isakeyword{theorem}, etc.\ & theorem statement with proof \\
-  \isakeyword{theorems}, etc.\ & redeclaration of theorems
+  \isakeyword{theorems}, etc.\ & redeclaration of theorems \\
+  \isakeyword{text}, etc.\ & document markup
 \end{tabular}
 \end{center}
 \hrule
@@ -137,7 +139,7 @@
 \ \ partial{\isacharunderscore}order\ {\isacharquery}le\ {\isasymLongrightarrow}\isanewline
 \isaindent{\ \ }partial{\isacharunderscore}order{\isachardot}less\ {\isacharquery}le\ {\isacharquery}x\ {\isacharquery}y\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}le\ {\isacharquery}x\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}%
 \end{isabelle}
-  At the same time, the locale is extended by syntax information
+  At the same time, the locale is extended by syntax transformations
   hiding this construction in the context of the locale.  That is,
   \isa{partial{\isacharunderscore}order{\isachardot}less\ le} is printed and parsed as infix
   \isa{{\isasymsqsubset}}.%
@@ -464,16 +466,6 @@
 \ \ \isacommand{end}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
-The definitions of \isa{is{\isacharunderscore}inf} and \isa{is{\isacharunderscore}sup} look
-  like ordinary definitions in theories.  Despite, what is going on
-  behind the scenes is more complex.  The definition of \isa{is{\isacharunderscore}inf}, say, creates a constant \isa{partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf} where
-  the locale parameters that occur in the definition of \isa{is{\isacharunderscore}inf}
-  are additional arguments.  Writing \isa{is{\isacharunderscore}inf\ x\ y\ inf} is just
-  a notational convenience for \isa{partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf\ op\ {\isasymsqsubseteq}\ x\ y\ inf}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
 Two commands are provided to inspect locales:
   \isakeyword{print\_locales} lists the names of all locales of the
   current theory; \isakeyword{print\_locale}~$n$ prints the parameters
@@ -499,7 +491,8 @@
   distributive lattices.
 
   With locales, this inheritance is achieved through \emph{import} of a
-  locale.  The import comes before the context elements.%
+  locale.  Import is a separate entity in the locale declaration.  If
+  present, it precedes the context elements.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
@@ -509,11 +502,8 @@
 \ \ \isakeyword{begin}%
 \begin{isamarkuptext}%
 These assumptions refer to the predicates for infimum
-  and supremum defined in \isa{partial{\isacharunderscore}order}.  In the current
-  implementation of locales, syntax from definitions of the imported
-  locale is unavailable in the locale declaration, neither are their
-  names.  Hence we refer to the constants of the theory.  The names
-  and syntax is available below, in the context of the locale.%
+  and supremum defined in \isa{partial{\isacharunderscore}order}.  We may now introduce
+  the notions of meet and join.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{definition}\isamarkupfalse%

--- a/doc-src/Locales/Locales/document/Examples1.tex	Sun Mar 29 17:38:01 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples1.tex	Tue Mar 31 21:25:08 2009 +0200
@@ -46,7 +46,7 @@
   theories is illustrated; interpretation in proofs is analogous.
 
   As an example, consider the type of natural numbers \isa{nat}.  The
-  order relation \isa{{\isasymle}} is a total order over \isa{nat},
+  relation \isa{{\isasymle}} is a total order over \isa{nat},
   divisibility \isa{dvd} is a distributive lattice.  We start with the
   interpretation that \isa{{\isasymle}} is a partial order.  The facilities of
   the interpretation command are explored in three versions.%
@@ -78,7 +78,7 @@
   instantiation}.  This is a list of terms, which refer to
   the parameters in the order of declaration in the locale.  The
   locale name is preceded by an optional \emph{interpretation
-  qualifier}.
+  qualifier}, here \isa{nat}.
 
   The command creates the goal%
 \footnote{Note that \isa{op} binds tighter than functions
@@ -125,10 +125,8 @@
   Here, \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}}
   represents the strict order, although \isa{{\isacharless}} is the natural
   strict order for \isa{nat}.  Interpretation allows to map concepts
-  introduced through definitions in locales to the corresponding
+  introduced by definitions in locales to the corresponding
   concepts of the theory.%
-\footnote{This applies not only to \isakeyword{definition} but also to
-  \isakeyword{inductive}, \isakeyword{fun} and \isakeyword{function}.}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

--- a/doc-src/Locales/Locales/document/Examples2.tex	Sun Mar 29 17:38:01 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples2.tex	Tue Mar 31 21:25:08 2009 +0200
@@ -22,7 +22,7 @@
 This is achieved by unfolding suitable equations during
   interpretation.  These equations are given after the keyword
   \isakeyword{where} and require proofs.  The revised command
-  that replaces \isa{{\isasymsqsubset}} by \isa{{\isacharless}}, is:%
+  that replaces \isa{{\isasymsqsubset}} by \isa{{\isacharless}} is:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

--- a/doc-src/Locales/Locales/document/Examples3.tex	Sun Mar 29 17:38:01 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Tue Mar 31 21:25:08 2009 +0200
@@ -68,19 +68,15 @@
 \endisadelimvisible
 %
 \begin{isamarkuptext}%
-The inner interpretation does not require an
-  elaborate new proof, it is immediate from the preceeding fact and
-  proved with ``.''.  Strict qualifiers are normally not necessary for
-  interpretations inside proofs, since these have only limited scope.
-
-  The above interpretation enriches the local proof context by
-  the very theorems also obtained in the interpretation from
-  Section~\ref{sec:po-first}, and \isa{nat{\isachardot}less{\isacharunderscore}def} may directly be
-  used to unfold the definition.  Theorems from the local
-  interpretation disappear after leaving the proof context --- that
-  is, after the closing \isakeyword{qed} --- and are
-  then replaced by those with the desired substitutions of the strict
-  order.%
+The inner interpretation does not require an elaborate new
+  proof, it is immediate from the preceding fact and proved with
+  ``.''.  It enriches the local proof context by the very theorems
+  also obtained in the interpretation from Section~\ref{sec:po-first},
+  and \isa{nat{\isachardot}less{\isacharunderscore}def} may directly be used to unfold the
+  definition.  Theorems from the local interpretation disappear after
+  leaving the proof context --- that is, after the closing
+  \isakeyword{qed} --- and are then replaced by those with the desired
+  substitutions of the strict order.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -139,7 +135,7 @@
 \ arith{\isacharplus}%
 \begin{isamarkuptxt}%
 For the first of the equations, we refer to the theorem
-  generated in the previous interpretation.%
+  shown in the previous interpretation.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \ \ \isacommand{show}\isamarkupfalse%
@@ -173,8 +169,7 @@
 \endisadelimvisible
 %
 \begin{isamarkuptext}%
-The interpretation that the relation \isa{{\isasymle}} is a total
-  order follows next.%
+Next follows that \isa{{\isasymle}} is a total order.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -191,7 +186,8 @@
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}total{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isachardoublequoteopen}total{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales\ arith\isanewline
 \isacommand{qed}\isamarkupfalse%
 \ {\isacharparenleft}rule\ nat{\isacharunderscore}less{\isacharunderscore}eq\ nat{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}join{\isacharunderscore}eq{\isacharparenright}{\isacharplus}%
@@ -203,7 +199,7 @@
 \endisadelimvisible
 %
 \begin{isamarkuptext}%
-Note that since the locale hierarchy reflects that total
+Since the locale hierarchy reflects that total
   orders are distributive lattices, an explicit interpretation of
   distributive lattices for the order relation on natural numbers is
   only necessary for mapping the definitions to the right operators on
@@ -268,7 +264,8 @@
 \isamarkuptrue%
 \isacommand{interpretation}\isamarkupfalse%
 \ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{where}\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq{\isacharcolon}\isanewline
+\ \ \ \ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 %
 \isadelimproof
 %
@@ -378,8 +375,8 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-Equations \isa{nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq} and \isa{nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq} are named since they are handy in the proof of
-  the subsequent interpretation.%
+Equations \isa{nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq} and \isa{nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq} are used in the main part the subsequent
+  interpretation.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -473,7 +470,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The full syntax of the interpretation commands is shown in
+The syntax of the interpretation commands is shown in
   Table~\ref{tab:commands}.  The grammar refers to
   \textit{expression}, which stands for a \emph{locale} expression.
   Locale expressions are discussed in the following section.%
@@ -493,13 +490,13 @@
   Inspecting the grammar of locale commands in
   Table~\ref{tab:commands} reveals that the import of a locale can be
   more than just a single locale.  In general, the import is a
-  \emph{locale expression}.  These enable to combine locales
+  \emph{locale expression}, which enables to combine locales
   and instantiate parameters.  A locale expression is a sequence of
   locale \emph{instances} followed by an optional \isakeyword{for}
   clause.  Each instance consists of a locale reference, which may be
   preceded by a qualifer and succeeded by instantiations of the
   parameters of that locale.  Instantiations may be either positional
-  or through explicit parameter argument pairs.
+  or through explicit mappings of parameters to arguments.
 
   Using a locale expression, a locale for order
   preserving maps can be declared in the following way.%
@@ -513,15 +510,17 @@
 \ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y\ {\isasymLongrightarrow}\ {\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 The second and third line contain the expression --- two
-  instances of the partial order locale with instantiations \isa{le}
+  instances of the partial order locale where the parameter is
+  instantiated to \isa{le}
   and \isa{le{\isacharprime}}, respectively.  The \isakeyword{for} clause consists
   of parameter declarations and is similar to the context element
   \isakeyword{fixes}.  The notable difference is that the
   \isakeyword{for} clause is part of the expression, and only
   parameters defined in the expression may occur in its instances.
 
-  Instances are \emph{morphisms} on locales.  Their effect on the
-  parameters is naturally lifted to terms, propositions and theorems,
+  Instances define \emph{morphisms} on locales.  Their effect on the
+  parameters is lifted to terms, propositions and theorems in the
+  canonical way,
   and thus to the assumptions and conclusions of a locale.  The
   assumption of a locale expression is the conjunction of the
   assumptions of the instances.  The conclusions of a sequence of
@@ -584,8 +583,9 @@
 \endisadeliminvisible
 %
 \begin{isamarkuptext}%
-This example reveals that there is no infix syntax for the strict
-  version of \isa{{\isasympreceq}}!  This can be declared through an abbreviation.%
+This example reveals that there is no infix syntax for the
+  strict operation associated with \isa{{\isasympreceq}}.  This can be declared
+  through an abbreviation.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{abbreviation}\isamarkupfalse%
@@ -593,17 +593,18 @@
 \ \ \ \ less{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymprec}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}less{\isacharprime}\ {\isasymequiv}\ partial{\isacharunderscore}order{\isachardot}less\ le{\isacharprime}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 Now the theorem is displayed nicely as
-  \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z}.%
+  \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
+  \begin{isabelle}%
+\ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z%
+\end{isabelle}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Qualifiers not only apply to theorem names, but also to names
-  introduced by definitions and abbreviations.  In locale
-  \isa{partial{\isacharunderscore}order} the full name of the strict order of \isa{{\isasymsqsubseteq}} is
-  \isa{le{\isachardot}less} and therefore \isa{le{\isacharprime}{\isachardot}less} is the full name of
-  the strict order of \isa{{\isasympreceq}}.  Hence, the equation in the
-  abbreviation above could have been also written as \isa{less{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}less}.%
+  introduced by definitions and abbreviations.  For example, in \isa{partial{\isacharunderscore}order} the name \isa{less} abbreviates \isa{op\ {\isasymsqsubset}}.  Therefore, in \isa{order{\isacharunderscore}preserving}
+  the qualified name \isa{le{\isachardot}less} abbreviates \isa{op\ {\isasymsqsubset}} and \isa{le{\isacharprime}{\isachardot}less} abbreviates \isa{op\ {\isasymprec}}.  Hence, the equation in the abbreviation
+  above could have been written more concisely as \isa{less{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}less}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -618,9 +619,9 @@
   instantiation terms than the instantiated locale's number of
   parameters.  In named instantiations, instantiation pairs for
   certain parameters may simply be omitted.  Untouched parameters are
-  declared by the locale expression and with their concrete syntax by
-  implicitly adding them to the beginning of the \isakeyword{for}
-  clause.
+  implicitly declared by the locale expression and with their concrete
+  syntax.  In the sequence of parameters, they appear before the
+  parameters from the \isakeyword{for} clause.
 
   The following locales illustrate this.  A map \isa{{\isasymphi}} is a
   lattice homomorphism if it preserves meet and join.%
@@ -630,10 +631,8 @@
 \ lattice{\isacharunderscore}hom\ {\isacharequal}\isanewline
 \ \ \ \ le{\isacharcolon}\ lattice\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ lattice\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
 \ \ \ \ \isakeyword{fixes}\ {\isasymphi}\isanewline
-\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}meet{\isacharcolon}\isanewline
-\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqinter}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}meet\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isakeyword{and}\ hom{\isacharunderscore}join{\isacharcolon}\isanewline
-\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}join\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}meet{\isacharcolon}\ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqinter}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}meet\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isakeyword{and}\ hom{\isacharunderscore}join{\isacharcolon}\ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}join\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
 \ \ \isacommand{abbreviation}\isamarkupfalse%
 \ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline
@@ -648,7 +647,7 @@
 \ \ \isacommand{locale}\isamarkupfalse%
 \ lattice{\isacharunderscore}end\ {\isacharequal}\ lattice{\isacharunderscore}hom\ {\isacharunderscore}\ le%
 \begin{isamarkuptext}%
-In this declaration, the first parameter of \isa{lattice{\isacharunderscore}hom}, \isa{le}, is untouched and then used to instantiate
+In this declaration, the first parameter of \isa{lattice{\isacharunderscore}hom}, \isa{le}, is untouched and is then used to instantiate
   the second parameter.  Its concrete syntax is preserved.%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -740,9 +739,10 @@
 \begin{isamarkuptext}%
 Theorems and other declarations --- syntax, in particular --- from
   the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example
-
-  \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
-  \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z}%
+  \isa{hom{\isacharunderscore}le}:
+  \begin{isabelle}%
+\ \ {\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y%
+\end{isabelle}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -872,7 +872,7 @@
 \end{tabular}
 \end{center}
 \hrule
-\caption{Syntax of Locale Commands (abridged).}
+\caption{Syntax of Locale Commands.}
 \label{tab:commands}
 \end{table}%
 \end{isamarkuptext}%