Updated chapters 1-5 to locale reimplementation.

--- a/doc-src/Locales/Locales/Examples.thy	Wed Mar 18 19:11:26 2009 +0100
+++ b/doc-src/Locales/Locales/Examples.thy	Wed Mar 18 22:14:58 2009 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory Examples
 imports Main GCD
 begin
@@ -137,9 +135,9 @@
   target for a block may be given with the \isakeyword{context}
   command.
 
-  In the block below, notions of infimum and supremum together with
-  theorems are introduced for partial orders.
-  *}
+  This style of working is illustrated in the block below, where
+  notions of infimum and supremum for partial orders are introduced,
+  together with theorems.  *}
 
   context partial_order begin
 
@@ -238,15 +236,19 @@
 
   end
 
-text {* In fact, many more theorems need to be shown for a usable
-  theory of partial orders.  The
-  above two serve as illustrative examples. *}
+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:
+text {* Two commands are provided to inspect locales:
   \isakeyword{print\_locales} lists the names of all locales of the
-  theory; \isakeyword{print\_locale}~$n$ prints the parameters and
-  assumptions of locale $n$; \isakeyword{print\_locale!}~$n$
+  current theory; \isakeyword{print\_locale}~$n$ prints the parameters
+  and assumptions of locale $n$; \isakeyword{print\_locale!}~$n$
   additionally outputs the conclusions.
 
   The syntax of the locale commands discussed in this tutorial is
@@ -255,11 +257,9 @@
   for full documentation.  *}
 
 
-section {* Import *}
+section {* Import \label{sec:import} *}
 
 text {* 
-\label{sec:import}
-
   Algebraic structures are commonly defined by adding operations and
   properties to existing structures.  For example, partial orders
   are extended to lattices and total orders.  Lattices are extended to
@@ -270,11 +270,11 @@
   *}
 
   locale lattice = partial_order +
-    assumes ex_inf: "\<exists>inf. partial_order.is_inf le x y inf"
-      and ex_sup: "\<exists>sup. partial_order.is_sup le x y sup"
+    assumes ex_inf: "\<exists>inf. is_inf x y inf"
+      and ex_sup: "\<exists>sup. is_sup x y sup"
   begin
 
-text {* Note that the assumptions above refer to the predicates for infimum
+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
@@ -537,9 +537,7 @@
     by (unfold less_def) blast
 
   locale distrib_lattice = lattice +
-    assumes meet_distr:
-      "lattice.meet le x (lattice.join le y z) =
-      lattice.join le (lattice.meet le x y) (lattice.meet le x z)"
+    assumes meet_distr: "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z"
 
   lemma (in distrib_lattice) join_distr:
     "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"  (* txt {* Jacobson I, p.\ 462 *} *)
@@ -600,11 +598,10 @@
 \end{figure}
   *}
 
-section {* Changing the Locale Hierarchy *}
+section {* Changing the Locale Hierarchy
+  \label{sec:changing-the-hierarchy} *}
 
 text {*
-\label{sec:changing-the-hierarchy}
-
   Total orders are lattices.  Hence, by deriving the lattice
   axioms for total orders, the hierarchy may be changed
   and @{text lattice} be placed between @{text partial_order}

--- a/doc-src/Locales/Locales/Examples1.thy	Wed Mar 18 19:11:26 2009 +0100
+++ b/doc-src/Locales/Locales/Examples1.thy	Wed Mar 18 22:14:58 2009 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory Examples1
 imports Examples
 begin
@@ -14,7 +12,7 @@
 
   The changes of the locale
   hierarchy from the previous sections are examples of
-  interpretations.  The command \isakeyword{interpretation} $l_1
+  interpretations.  The command \isakeyword{sublocale} $l_1
   \subseteq l_2$ is said to \emph{interpret} locale $l_2$ in the
   context of $l_1$.  It causes all theorems of $l_2$ to be made
   available in $l_1$.  The interpretation is \emph{dynamic}: not only
@@ -27,17 +25,17 @@
   Theorems added to locales will be propagated to theories.
   In this section the interpretation in
   theories is illustrated; interpretation in proofs is analogous.
-  As an example consider, the type of natural numbers @{typ nat}.  The
+
+  As an example, consider the type of natural numbers @{typ nat}.  The
   order relation @{text \<le>} is a total order over @{typ nat},
-  divisibility @{text dvd} is a distributive lattice.
-
-  We start with the
+  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.
   *}
 
 
-subsection {* First Version: Replacement of Parameters Only \label{sec:po-first} *}
+subsection {* First Version: Replacement of Parameters Only
+  \label{sec:po-first} *}
 
 text {*
   In the most basic form, interpretation just replaces the locale
@@ -45,7 +43,7 @@
   @{text partial_order} in the global context of the theory.  The
   parameter @{term le} is replaced by @{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"}. *} 
 
-  interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  interpretation %visible nat!: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
 txt {* The locale name is succeeded by a \emph{parameter
   instantiation}.  In general, this is a list of terms, which refer to
   the parameters in the order of declaration in the locale.  The
@@ -53,10 +51,10 @@
   which is used to qualify names from the locale in the global
   context.
 
-  The command creates the goal @{subgoals [display]} which can be shown
-  easily:%
+  The command creates the goal%
 \footnote{Note that @{text op} binds tighter than functions
   application: parentheses around @{text "op \<le>"} are not necessary.}
+  @{subgoals [display]} which can be shown easily:
  *}
     by unfold_locales auto
 
@@ -64,12 +62,14 @@
   interpreted for natural numbers, for example @{thm [source]
   nat.trans}: @{thm [display, indent=2] nat.trans}
 
-  In order to avoid unwanted hiding of theorems, interpretation
-  accepts a qualifier, @{text nat} in the example, which is applied to
-  all names processed by the
-  interpretation.  If present the qualifier is mandatory --- that is,
-  the above theorem cannot be referred to simply as @{text trans}.
-  *}
+  Interpretation accepts a qualifier, @{text nat} in the example,
+  which is applied to all names processed by the interpretation.  If
+  followed by an exclamation point the qualifier is mandatory --- that
+  is, the above theorem cannot be referred to simply by @{text trans}.
+  A qualifier succeeded by an exclamation point is called
+  \emph{strict}.  It prevents unwanted hiding of theorems.  It is
+  advisable to use strict qualifiers for all interpretations in
+  theories.  *}
 
 
 subsection {* Second Version: Replacement of Definitions *}
@@ -78,9 +78,9 @@
   @{thm [source] nat.less_le_trans}: @{thm [display, indent=2]
   nat.less_le_trans}
   Here, @{term "partial_order.less (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"}
-  represents the strict order, although @{text "<"} is defined on
-  @{typ nat}.  Interpretation enables to map concepts
-  introduced in locales through definitions to the corresponding
+  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}.} 

--- a/doc-src/Locales/Locales/Examples2.thy	Wed Mar 18 19:11:26 2009 +0100
+++ b/doc-src/Locales/Locales/Examples2.thy	Wed Mar 18 22:14:58 2009 +0100
@@ -1,19 +1,17 @@
-(* $Id$ *)
-
 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,
-  replacing @{text "\<sqsubset>"} by @{text "<"}, is: *}
+  \isakeyword{where} and require proofs.  The revised command
+  that replaces @{text "\<sqsubset>"} by @{text "<"}, is: *}
 
-interpretation %visible nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool"
+interpretation %visible nat!: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool"
   where "partial_order.less op \<le> (x::nat) y = (x < y)"
 proof -
   txt {* The goals are @{subgoals [display]}
-    The proof that @{text \<le>} is a partial order is a above. *}
+    The proof that @{text \<le>} is a partial order is as above. *}
   show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
     by unfold_locales auto
   txt {* The second goal is shown by unfolding the

--- a/doc-src/Locales/Locales/Examples3.thy	Wed Mar 18 19:11:26 2009 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy	Wed Mar 18 22:14:58 2009 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory Examples3
 imports Examples
 begin
@@ -16,27 +14,29 @@
   \isakeyword{interpret}).  This interpretation is inside the proof of the global
   interpretation.  The third revision of the example illustrates this.  *}
 
-interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  where "partial_order.less (op \<le>) (x::nat) y = (x < y)"
+interpretation %visible nat!: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  where "partial_order.less op \<le> (x::nat) y = (x < y)"
 proof -
   show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
     by unfold_locales auto
   then interpret nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool" .
-  show "partial_order.less (op \<le>) (x::nat) y = (x < y)"
+  show "partial_order.less op \<le> (x::nat) y = (x < y)"
     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 ``.''.
-  This interpretation enriches the local proof context by
+  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. *}
+  order.  *}
 
 
 subsection {* Further Interpretations *}
@@ -48,7 +48,7 @@
   interpretation is reproduced in order to give an example of a more
   elaborate interpretation proof.  *}
 
-interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+interpretation %visible nat!: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
   where "lattice.meet op \<le> (x::nat) y = min x y"
     and "lattice.join op \<le> (x::nat) y = max x y"
 proof -
@@ -73,7 +73,7 @@
 text {* That the relation @{text \<le>} is a total order completes this
   sequence of interpretations. *}
 
-interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+interpretation %visible nat!: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
   by unfold_locales arith
 
 text {* Theorems that are available in the theory at this point are shown in
@@ -142,10 +142,11 @@
     done
 qed
 
-text {* Note that there is no symbol for strict divisibility.  Instead,
-  interpretation substitutes @{term "x dvd y \<and> x \<noteq> y"}.   *}
+text {* Note that in Isabelle/HOL there is no symbol for strict
+  divisibility.  Instead, interpretation substitutes @{term "x dvd y \<and>
+  x \<noteq> y"}.  *}
 
-interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
+interpretation nat_dvd!: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   where nat_dvd_meet_eq:
       "lattice.meet op dvd = gcd"
     and nat_dvd_join_eq:
@@ -198,7 +199,7 @@
 lemma %invisible gcd_lcm_distr:
   "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry
 
-interpretation %visible nat_dvd:
+interpretation %visible nat_dvd!:
   distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   apply unfold_locales
   txt {* @{subgoals [display]} *}
@@ -232,8 +233,8 @@
 text {*
   The full syntax of the interpretation commands is shown in
   Table~\ref{tab:commands}.  The grammar refers to
-  \textit{expr}, which stands for a \emph{locale} expression.  Locale
-  expressions are discussed in Section~\ref{sec:expressions}.
+  \textit{expression}, which stands for a \emph{locale} expression.
+  Locale expressions are discussed in the following section.
   *}
 
 

--- a/doc-src/Locales/Locales/document/Examples.tex	Wed Mar 18 19:11:26 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples.tex	Wed Mar 18 22:14:58 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{Examples}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
@@ -197,8 +195,9 @@
   target for a block may be given with the \isakeyword{context}
   command.
 
-  In the block below, notions of infimum and supremum together with
-  theorems are introduced for partial orders.%
+  This style of working is illustrated in the block below, where
+  notions of infimum and supremum for partial orders are introduced,
+  together with theorems.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{context}\isamarkupfalse%
@@ -465,17 +464,20 @@
 \ \ \isacommand{end}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
-In fact, many more theorems need to be shown for a usable
-  theory of partial orders.  The
-  above two serve as illustrative examples.%
+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
-  theory; \isakeyword{print\_locale}~$n$ prints the parameters and
-  assumptions of locale $n$; \isakeyword{print\_locale!}~$n$
+  current theory; \isakeyword{print\_locale}~$n$ prints the parameters
+  and assumptions of locale $n$; \isakeyword{print\_locale!}~$n$
   additionally outputs the conclusions.
 
   The syntax of the locale commands discussed in this tutorial is
@@ -485,14 +487,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Import%
+\isamarkupsection{Import \label{sec:import}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-\label{sec:import}
-
-  Algebraic structures are commonly defined by adding operations and
+Algebraic structures are commonly defined by adding operations and
   properties to existing structures.  For example, partial orders
   are extended to lattices and total orders.  Lattices are extended to
   distributive lattices.
@@ -503,11 +503,11 @@
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
 \ lattice\ {\isacharequal}\ partial{\isacharunderscore}order\ {\isacharplus}\isanewline
-\ \ \ \ \isakeyword{assumes}\ ex{\isacharunderscore}inf{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}inf{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf\ le\ x\ y\ inf{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isakeyword{and}\ ex{\isacharunderscore}sup{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}sup{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}sup\ le\ x\ y\ sup{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{assumes}\ ex{\isacharunderscore}inf{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}inf{\isachardot}\ is{\isacharunderscore}inf\ x\ y\ inf{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isakeyword{and}\ ex{\isacharunderscore}sup{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}sup{\isachardot}\ is{\isacharunderscore}sup\ x\ y\ sup{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{begin}%
 \begin{isamarkuptext}%
-Note that the assumptions above refer to the predicates for infimum
+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
@@ -1110,9 +1110,7 @@
 \isanewline
 \ \ \isacommand{locale}\isamarkupfalse%
 \ distrib{\isacharunderscore}lattice\ {\isacharequal}\ lattice\ {\isacharplus}\isanewline
-\ \ \ \ \isakeyword{assumes}\ meet{\isacharunderscore}distr{\isacharcolon}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}meet\ le\ x\ {\isacharparenleft}lattice{\isachardot}join\ le\ y\ z{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ lattice{\isachardot}join\ le\ {\isacharparenleft}lattice{\isachardot}meet\ le\ x\ y{\isacharparenright}\ {\isacharparenleft}lattice{\isachardot}meet\ le\ x\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{assumes}\ meet{\isacharunderscore}distr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqinter}\ {\isacharparenleft}y\ {\isasymsqunion}\ z{\isacharparenright}\ {\isacharequal}\ x\ {\isasymsqinter}\ y\ {\isasymsqunion}\ x\ {\isasymsqinter}\ z{\isachardoublequoteclose}\isanewline
 \isanewline
 \ \ \isacommand{lemma}\isamarkupfalse%
 \ {\isacharparenleft}\isakeyword{in}\ distrib{\isacharunderscore}lattice{\isacharparenright}\ join{\isacharunderscore}distr{\isacharcolon}\isanewline
@@ -1206,14 +1204,13 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Changing the Locale Hierarchy%
+\isamarkupsection{Changing the Locale Hierarchy
+  \label{sec:changing-the-hierarchy}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-\label{sec:changing-the-hierarchy}
-
-  Total orders are lattices.  Hence, by deriving the lattice
+Total orders are lattices.  Hence, by deriving the lattice
   axioms for total orders, the hierarchy may be changed
   and \isa{lattice} be placed between \isa{partial{\isacharunderscore}order}
   and \isa{total{\isacharunderscore}order}, as shown in Figure~\ref{fig:lattices}(b).

--- a/doc-src/Locales/Locales/document/Examples1.tex	Wed Mar 18 19:11:26 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples1.tex	Wed Mar 18 22:14:58 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{Examples{\isadigit{1}}}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
@@ -33,7 +31,7 @@
 
   The changes of the locale
   hierarchy from the previous sections are examples of
-  interpretations.  The command \isakeyword{interpretation} $l_1
+  interpretations.  The command \isakeyword{sublocale} $l_1
   \subseteq l_2$ is said to \emph{interpret} locale $l_2$ in the
   context of $l_1$.  It causes all theorems of $l_2$ to be made
   available in $l_1$.  The interpretation is \emph{dynamic}: not only
@@ -46,17 +44,17 @@
   Theorems added to locales will be propagated to theories.
   In this section the interpretation in
   theories is illustrated; interpretation in proofs is analogous.
-  As an example consider, the type of natural numbers \isa{nat}.  The
+
+  As an example, consider the type of natural numbers \isa{nat}.  The
   order relation \isa{{\isasymle}} is a total order over \isa{nat},
-  divisibility \isa{dvd} is a distributive lattice.
-
-  We start with the
+  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.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{First Version: Replacement of Parameters Only \label{sec:po-first}%
+\isamarkupsubsection{First Version: Replacement of Parameters Only
+  \label{sec:po-first}%
 }
 \isamarkuptrue%
 %
@@ -74,7 +72,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}%
+\ nat{\isacharbang}{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}%
 \begin{isamarkuptxt}%
 The locale name is succeeded by a \emph{parameter
   instantiation}.  In general, this is a list of terms, which refer to
@@ -83,12 +81,12 @@
   which is used to qualify names from the locale in the global
   context.
 
-  The command creates the goal \begin{isabelle}%
+  The command creates the goal%
+\footnote{Note that \isa{op} binds tighter than functions
+  application: parentheses around \isa{op\ {\isasymle}} are not necessary.}
+  \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ partial{\isacharunderscore}order\ op\ {\isasymle}%
-\end{isabelle} which can be shown
-  easily:%
-\footnote{Note that \isa{op} binds tighter than functions
-  application: parentheses around \isa{op\ {\isasymle}} are not necessary.}%
+\end{isabelle} which can be shown easily:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \ \ \ \ \isacommand{by}\isamarkupfalse%
@@ -106,11 +104,14 @@
 \ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymle}\ {\isacharquery}z%
 \end{isabelle}
 
-  In order to avoid unwanted hiding of theorems, interpretation
-  accepts a qualifier, \isa{nat} in the example, which is applied to
-  all names processed by the
-  interpretation.  If present the qualifier is mandatory --- that is,
-  the above theorem cannot be referred to simply as \isa{trans}.%
+  Interpretation accepts a qualifier, \isa{nat} in the example,
+  which is applied to all names processed by the interpretation.  If
+  followed by an exclamation point the qualifier is mandatory --- that
+  is, the above theorem cannot be referred to simply by \isa{trans}.
+  A qualifier succeeded by an exclamation point is called
+  \emph{strict}.  It prevents unwanted hiding of theorems.  It is
+  advisable to use strict qualifiers for all interpretations in
+  theories.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -125,9 +126,9 @@
 \isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}z%
 \end{isabelle}
   Here, \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}}
-  represents the strict order, although \isa{{\isacharless}} is defined on
-  \isa{nat}.  Interpretation enables to map concepts
-  introduced in locales through definitions to the corresponding
+  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
   concepts of the theory.%
 \footnote{This applies not only to \isakeyword{definition} but also to
   \isakeyword{inductive}, \isakeyword{fun} and \isakeyword{function}.}%

--- a/doc-src/Locales/Locales/document/Examples2.tex	Wed Mar 18 19:11:26 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples2.tex	Wed Mar 18 22:14:58 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{Examples{\isadigit{2}}}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
@@ -23,8 +21,8 @@
 \begin{isamarkuptext}%
 This is achieved by unfolding suitable equations during
   interpretation.  These equations are given after the keyword
-  \isakeyword{where} and require proofs.  The revised command,
-  replacing \isa{{\isasymsqsubset}} by \isa{{\isacharless}}, is:%
+  \isakeyword{where} and require proofs.  The revised command
+  that replaces \isa{{\isasymsqsubset}} by \isa{{\isacharless}}, is:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -34,7 +32,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ nat{\isacharbang}{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}%
@@ -43,7 +41,7 @@
 \ {\isadigit{1}}{\isachardot}\ partial{\isacharunderscore}order\ op\ {\isasymle}\isanewline
 \ {\isadigit{2}}{\isachardot}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ x\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}%
 \end{isabelle}
-    The proof that \isa{{\isasymle}} is a partial order is a above.%
+    The proof that \isa{{\isasymle}} is a partial order is as above.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \ \ \isacommand{show}\isamarkupfalse%

--- a/doc-src/Locales/Locales/document/Examples3.tex	Wed Mar 18 19:11:26 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Wed Mar 18 22:14:58 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{Examples{\isadigit{3}}}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
@@ -43,8 +41,8 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ {\isacharparenleft}op\ {\isasymle}{\isacharparenright}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ nat{\isacharbang}{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
@@ -56,7 +54,7 @@
 \ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ {\isacharparenleft}op\ {\isasymle}{\isacharparenright}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
 \ nat{\isachardot}less{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
 \ auto\isanewline
@@ -72,8 +70,10 @@
 \begin{isamarkuptext}%
 The inner interpretation does not require an
   elaborate new proof, it is immediate from the preceeding fact and
-  proved with ``.''.
-  This interpretation enriches the local proof context by
+  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
@@ -104,7 +104,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ nat{\isacharbang}{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{where}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
@@ -174,7 +174,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ nat{\isacharbang}{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales\ arith%
 \endisatagvisible
@@ -280,12 +280,12 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-Note that there is no symbol for strict divisibility.  Instead,
-  interpretation substitutes \isa{x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y}.%
+Note that in Isabelle/HOL there is no symbol for strict
+  divisibility.  Instead, interpretation substitutes \isa{x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ nat{\isacharunderscore}dvd{\isacharbang}{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{where}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\isanewline
 \ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\isanewline
@@ -381,7 +381,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline
+\ nat{\isacharunderscore}dvd{\isacharbang}{\isacharcolon}\isanewline
 \ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{apply}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales%
@@ -439,8 +439,8 @@
 \begin{isamarkuptext}%
 The full syntax of the interpretation commands is shown in
   Table~\ref{tab:commands}.  The grammar refers to
-  \textit{expr}, which stands for a \emph{locale} expression.  Locale
-  expressions are discussed in Section~\ref{sec:expressions}.%
+  \textit{expression}, which stands for a \emph{locale} expression.
+  Locale expressions are discussed in the following section.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %