# HG changeset patch
# User ballarin
# Date 1232393828 -3600
# Node ID 937baa077df272183d8ec081001e9f0873e31fde
# Parent  3c6cd80a48541e152c03aee9f82d7a39eaf3b3b4
Fixed tutorial to compile with new locales; grammar of new locale commands.

diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/Examples.thy
--- a/doc-src/Locales/Locales/Examples.thy	Tue Dec 30 16:50:46 2008 +0100
+++ b/doc-src/Locales/Locales/Examples.thy	Mon Jan 19 20:37:08 2009 +0100
@@ -608,9 +608,9 @@
   and @{text lattice} be placed between @{text partial_order}
   and @{text total_order}, as shown in Figure~\ref{fig:lattices}(b).
   Changes to the locale hierarchy may be declared
-  with the \isakeyword{interpretation} command. *}
+  with the \isakeyword{sublocale} command. *}
 
-  interpretation %visible total_order \<subseteq> lattice
+  sublocale %visible total_order \<subseteq> lattice
 
 txt {* This enters the context of locale @{text total_order}, in
   which the goal @{subgoals [display]} must be shown.  First, the
@@ -652,7 +652,7 @@
 
 text {* Similarly, total orders are distributive lattices. *}
 
-  interpretation total_order \<subseteq> distrib_lattice
+  sublocale total_order \<subseteq> distrib_lattice
   proof unfold_locales
     fix %"proof" x y z
     show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/Examples1.thy
--- a/doc-src/Locales/Locales/Examples1.thy	Tue Dec 30 16:50:46 2008 +0100
+++ b/doc-src/Locales/Locales/Examples1.thy	Mon Jan 19 20:37:08 2009 +0100
@@ -45,7 +45,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
diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/Examples2.thy
--- a/doc-src/Locales/Locales/Examples2.thy	Tue Dec 30 16:50:46 2008 +0100
+++ b/doc-src/Locales/Locales/Examples2.thy	Mon Jan 19 20:37:08 2009 +0100
@@ -9,7 +9,7 @@
   \isakeyword{where} and require proofs.  The revised command,
   replacing @{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]}
diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/Examples3.thy
--- a/doc-src/Locales/Locales/Examples3.thy	Tue Dec 30 16:50:46 2008 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy	Mon Jan 19 20:37:08 2009 +0100
@@ -16,12 +16,12 @@
   \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"]
+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"] .
+  then interpret nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool" .
   show "partial_order.less (op \<le>) (x::nat) y = (x < y)"
     unfolding nat.less_def by auto
 qed
@@ -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 -
@@ -63,7 +63,7 @@
     by arith+
   txt {* In order to show the equations, we put ourselves in a
     situation where the lattice theorems can be used in a convenient way. *}
-  then interpret nat: lattice ["op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"] .
+  then interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
   show "lattice.meet op \<le> (x::nat) y = min x y"
     by (bestsimp simp: nat.meet_def nat.is_inf_def)
   show "lattice.join op \<le> (x::nat) y = max x y"
@@ -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
@@ -130,12 +130,12 @@
   but not a total order.  Interpretation again proceeds
   incrementally. *}
 
-interpretation nat_dvd: partial_order ["op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"]
+interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   where "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)
-  then interpret nat_dvd: partial_order ["op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"] .
+  then interpret nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
   show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
     apply (unfold nat_dvd.less_def)
     apply auto
@@ -145,7 +145,7 @@
 text {* Note that 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:
@@ -159,7 +159,7 @@
     apply (rule_tac x = "lcm x y" in exI)
     apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
     done
-  then interpret nat_dvd: lattice ["op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"] .
+  then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
   show "lattice.meet op dvd = gcd"
     apply (auto simp add: expand_fun_eq)
     apply (unfold nat_dvd.meet_def)
@@ -203,7 +203,7 @@
 ML %invisible {* reset quick_and_dirty *}
   
 interpretation %visible nat_dvd:
-  distrib_lattice ["op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"]
+  distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   apply unfold_locales
   txt {* @{subgoals [display]} *}
   apply (unfold nat_dvd_meet_eq nat_dvd_join_eq)
@@ -262,7 +262,7 @@
   preserving maps can be declared in the following way.  *}
 
   locale order_preserving =
-    partial_order + partial_order le' (infixl "\<preceq>" 50) +
+    le: partial_order + le': partial_order le' for le' (infixl "\<preceq>" 50) +
     fixes \<phi> :: "'a \<Rightarrow> 'b"
     assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y"
 
@@ -300,7 +300,7 @@
 text {*
   @{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
 
-  @{thm [source] le_le'_\<phi>.hom_le}: @{thm le_le'_\<phi>.hom_le}
+  @{thm [source] hom_le}: @{thm hom_le}
   *}
 
 text {* When renaming a locale, the morphism is also applied
@@ -331,7 +331,7 @@
 text {* Two more locales illustrate working with locale expressions.
   A map @{text \<phi>} is a lattice homomorphism if it preserves meet and join. *}
 
-  locale lattice_hom = lattice + lattice le' (infixl "\<preceq>" 50) +
+  locale lattice_hom = le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
     fixes \<phi>
     assumes hom_meet:
 	"\<phi> (lattice.meet le x y) = lattice.meet le' (\<phi> x) (\<phi> y)"
@@ -346,7 +346,7 @@
 text {* A homomorphism is an endomorphism if both orders coincide. *}
 
   locale lattice_end =
-    lattice_hom le (infixl "\<sqsubseteq>" 50) le (infixl "\<sqsubseteq>" 50)
+    lattice_hom le le for le (infixl "\<sqsubseteq>" 50)
 
 text {* The inheritance diagram of the situation we have now is shown
   in Figure~\ref{fig:hom}, where the dashed line depicts an
@@ -395,7 +395,7 @@
   preserving.  As the final example of this section, a locale
   interpretation is used to assert this. *}
 
-  interpretation lattice_hom \<subseteq> order_preserving proof unfold_locales
+  sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales
     fix x y
     assume "x \<sqsubseteq> y"
     then have "y = (x \<squnion> y)" by (simp add: le.join_connection)
@@ -448,7 +448,9 @@
 
   \textit{attr-name} & ::=
   & \textit{name} $|$ \textit{attribute} $|$
-    \textit{name} \textit{attribute} \\[2ex]
+    \textit{name} \textit{attribute} \\
+  \textit{qualifier} & ::=
+  & \textit{name} [``\textbf{!}''] \\[2ex]
 
   \multicolumn{3}{l}{Context Elements} \\
 
@@ -488,19 +490,23 @@
 
   \multicolumn{3}{l}{Locale Expressions} \\
 
-  \textit{rename} & ::=
-  & \textit{name} [ \textit{mixfix} ] $|$ ``\textbf{\_}'' \\
-  \textit{expr}  & ::= 
-  & \textit{renamed-expr} ( ``\textbf{+}'' \textit{renamed-expr} )$^*$ \\
-  \textit{renamed-expr} & ::=
-  & ( \textit{qualified-name} $|$
-    ``\textbf{(}'' \textit{expr} ``\textbf{)}'' ) \textit{rename}$^*$ \\[2ex]
+  \textit{pos-insts} & ::=
+  & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\
+  \textit{named-insts} & ::=
+  & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term}
+  ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
+  \textit{instance} & ::=
+  & [ \textit{qualifier} \textbf{:} ]
+    \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
+  \textit{expression}  & ::= 
+  & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
+    [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
 
   \multicolumn{3}{l}{Declaration of Locales} \\
 
   \textit{locale} & ::=
   & \textit{element}$^+$ \\
-  & | & \textit{locale-expr} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
+  & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
   \textit{toplevel} & ::=
   & \textbf{locale} \textit{name} [ ``\textbf{=}''
     \textit{locale} ] \\[2ex]
@@ -509,19 +515,17 @@
 
   \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ]
     \textit{prop} \\
-  \textit{insts} & ::= & [ ``\textbf{[}'' \textit{term}$^+$
-    ``\textbf{]}'' ] \\
-  & & [ \textbf{where} \textit{equation} ( \textbf{and}
-    \textit{equation} )$^*$ ] \\
+  \textit{equations} & ::= &  \textbf{where} \textit{equation} ( \textbf{and}
+    \textit{equation} )$^*$  \\
   \textit{toplevel} & ::=
-  & \textbf{interpretation} \textit{name} ( ``$<$'' $|$
-    ``$\subseteq$'' ) \textit{expr} \textit{proof} \\
+  & \textbf{sublocale} \textit{name} ( ``$<$'' $|$
+    ``$\subseteq$'' ) \textit{expression} \textit{proof} \\
   & |
-  & \textbf{interpretation} [ \textit{attr-name} ``\textbf{:}'' ]
-    \textit{expr} \textit{insts} \textit{proof} \\
+  & \textbf{interpretation}
+    \textit{expression} [ \textit{equations} ] \textit{proof} \\
   & |
-  & \textbf{interpret} [ \textit{attr-name} ``\textbf{:}'' ]
-    \textit{expr} \textit{insts} \textit{proof} \\[2ex]
+  & \textbf{interpret}
+    \textit{expression} \textit{proof} \\[2ex]
 
   \multicolumn{3}{l}{Diagnostics} \\
 
@@ -531,7 +535,7 @@
 \end{tabular}
 \end{center}
 \hrule
-\caption{Syntax of Locale Commands.}
+\caption{Syntax of Locale Commands (abrigded).}
 \label{tab:commands}
 \end{table}
   *}
diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/document/Examples.tex
--- a/doc-src/Locales/Locales/document/Examples.tex	Tue Dec 30 16:50:46 2008 +0100
+++ b/doc-src/Locales/Locales/document/Examples.tex	Mon Jan 19 20:37:08 2009 +0100
@@ -1213,7 +1213,7 @@
   and \isa{lattice} be placed between \isa{partial{\isacharunderscore}order}
   and \isa{total{\isacharunderscore}order}, as shown in Figure~\ref{fig:lattices}(b).
   Changes to the locale hierarchy may be declared
-  with the \isakeyword{interpretation} command.%
+  with the \isakeyword{sublocale} command.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1222,7 +1222,7 @@
 \endisadelimvisible
 %
 \isatagvisible
-\isacommand{interpretation}\isamarkupfalse%
+\isacommand{sublocale}\isamarkupfalse%
 \ total{\isacharunderscore}order\ {\isasymsubseteq}\ lattice%
 \begin{isamarkuptxt}%
 This enters the context of locale \isa{total{\isacharunderscore}order}, in
@@ -1325,7 +1325,7 @@
 Similarly, total orders are distributive lattices.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \isacommand{interpretation}\isamarkupfalse%
+\ \ \isacommand{sublocale}\isamarkupfalse%
 \ total{\isacharunderscore}order\ {\isasymsubseteq}\ distrib{\isacharunderscore}lattice\isanewline
 %
 \isadelimproof
diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/document/Examples1.tex
--- a/doc-src/Locales/Locales/document/Examples1.tex	Tue Dec 30 16:50:46 2008 +0100
+++ b/doc-src/Locales/Locales/document/Examples1.tex	Mon Jan 19 20:37:08 2009 +0100
@@ -74,7 +74,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}%
+\ nat{\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
diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/document/Examples2.tex
--- a/doc-src/Locales/Locales/document/Examples2.tex	Tue Dec 30 16:50:46 2008 +0100
+++ b/doc-src/Locales/Locales/document/Examples2.tex	Mon Jan 19 20:37:08 2009 +0100
@@ -34,7 +34,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+\ nat{\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}%
diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/document/Examples3.tex
--- a/doc-src/Locales/Locales/document/Examples3.tex	Tue Dec 30 16:50:46 2008 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Mon Jan 19 20:37:08 2009 +0100
@@ -43,7 +43,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+\ 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
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
@@ -53,7 +53,7 @@
 \ unfold{\isacharunderscore}locales\ auto\isanewline
 \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{interpret}\isamarkupfalse%
-\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ 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
@@ -91,8 +91,8 @@
 \begin{isamarkuptext}%
 Further interpretations are necessary to reuse theorems from
   the other locales.  In \isa{lattice} the operations \isa{{\isasymsqinter}} and
-  \isa{{\isasymsqunion}} are substituted by \isa{ord{\isacharunderscore}class{\isachardot}min} and
-  \isa{ord{\isacharunderscore}class{\isachardot}max}.  The entire proof for the
+  \isa{{\isasymsqunion}} are substituted by \isa{min} and
+  \isa{max}.  The entire proof for the
   interpretation is reproduced in order to give an example of a more
   elaborate interpretation proof.%
 \end{isamarkuptext}%
@@ -104,7 +104,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+\ nat{\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%
@@ -143,7 +143,7 @@
 \isamarkuptrue%
 \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{interpret}\isamarkupfalse%
-\ nat{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
@@ -174,7 +174,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ total{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+\ nat{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales\ arith%
 \endisatagvisible
@@ -196,11 +196,11 @@
   \isa{nat{\isachardot}less{\isacharunderscore}def} from locale \isa{partial{\isacharunderscore}order}: \\
   \quad \isa{{\isacharparenleft}{\isacharquery}x\ {\isacharless}\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}} \\
   \isa{nat{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\
-  \quad \isa{ord{\isacharunderscore}class{\isachardot}min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\
+  \quad \isa{min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\
   \isa{nat{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\
-  \quad \isa{ord{\isacharunderscore}class{\isachardot}max\ {\isacharquery}x\ {\isacharparenleft}ord{\isacharunderscore}class{\isachardot}min\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ ord{\isacharunderscore}class{\isachardot}min\ {\isacharparenleft}ord{\isacharunderscore}class{\isachardot}max\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}ord{\isacharunderscore}class{\isachardot}max\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
+  \quad \isa{lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharparenleft}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
   \isa{nat{\isachardot}less{\isacharunderscore}total} from locale \isa{total{\isacharunderscore}order}: \\
-  \quad \isa{{\isacharquery}x\ {\isacharless}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}y\ {\isacharless}\ {\isacharquery}x}
+  \quad \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymor}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}y\ {\isacharquery}x}
 \end{tabular}
 \end{center}
 \hrule
@@ -244,7 +244,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+\ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{where}\ {\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
@@ -260,7 +260,7 @@
 \ unfold{\isacharunderscore}locales\ {\isacharparenleft}auto\ simp{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}\isanewline
 \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{interpret}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{show}\isamarkupfalse%
 \ {\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
@@ -285,7 +285,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+\ nat{\isacharunderscore}dvd{\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
@@ -316,7 +316,7 @@
 \isanewline
 \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{interpret}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
@@ -390,7 +390,7 @@
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
 \ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline
-\ \ distrib{\isacharunderscore}lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+\ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{apply}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales%
 \begin{isamarkuptxt}%
@@ -434,7 +434,7 @@
   \isa{nat{\isacharunderscore}dvd{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\
   \quad \isa{gcd\ {\isacharquery}x\ {\isacharquery}y\ dvd\ {\isacharquery}x} \\
   \isa{nat{\isacharunderscore}dvd{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\
-  \quad \isa{lcm\ {\isacharquery}x\ {\isacharparenleft}gcd\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ gcd\ {\isacharparenleft}lcm\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lcm\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
+  \quad \isa{lattice{\isachardot}join\ op\ dvd\ {\isacharquery}x\ {\isacharparenleft}lattice{\isachardot}meet\ op\ dvd\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ op\ dvd\ {\isacharparenleft}lattice{\isachardot}join\ op\ dvd\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lattice{\isachardot}join\ op\ dvd\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
 \end{tabular}
 \end{center}
 \hrule
@@ -476,7 +476,7 @@
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
 \ order{\isacharunderscore}preserving\ {\isacharequal}\isanewline
-\ \ \ \ partial{\isacharunderscore}order\ {\isacharplus}\ partial{\isacharunderscore}order\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
+\ \ \ \ le{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
 \ \ \ \ \isakeyword{fixes}\ {\isasymphi}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y\ {\isasymLongrightarrow}\ {\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
@@ -531,7 +531,7 @@
 \begin{isamarkuptext}%
 \isa{le{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymsqsubseteq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}z}
 
-  \isa{le{\isacharunderscore}le{\isacharprime}{\isacharunderscore}{\isasymphi}{\isachardot}hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}%
+  \isa{hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -589,7 +589,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
-\ lattice{\isacharunderscore}hom\ {\isacharequal}\ lattice\ {\isacharplus}\ lattice\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
+\ lattice{\isacharunderscore}hom\ {\isacharequal}\ 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}lattice{\isachardot}meet\ le\ x\ y{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ le{\isacharprime}\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
@@ -608,7 +608,7 @@
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
 \ lattice{\isacharunderscore}end\ {\isacharequal}\isanewline
-\ \ \ \ lattice{\isacharunderscore}hom\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
+\ \ \ \ lattice{\isacharunderscore}hom\ le\ le\ \isakeyword{for}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
 \begin{isamarkuptext}%
 The inheritance diagram of the situation we have now is shown
   in Figure~\ref{fig:hom}, where the dashed line depicts an
@@ -659,7 +659,7 @@
   interpretation is used to assert this.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \isacommand{interpretation}\isamarkupfalse%
+\ \ \isacommand{sublocale}\isamarkupfalse%
 \ lattice{\isacharunderscore}hom\ {\isasymsubseteq}\ order{\isacharunderscore}preserving%
 \isadelimproof
 \ %
@@ -741,7 +741,9 @@
 
   \textit{attr-name} & ::=
   & \textit{name} $|$ \textit{attribute} $|$
-    \textit{name} \textit{attribute} \\[2ex]
+    \textit{name} \textit{attribute} \\
+  \textit{qualifier} & ::=
+  & \textit{name} [``\textbf{!}''] \\[2ex]
 
   \multicolumn{3}{l}{Context Elements} \\
 
@@ -781,19 +783,23 @@
 
   \multicolumn{3}{l}{Locale Expressions} \\
 
-  \textit{rename} & ::=
-  & \textit{name} [ \textit{mixfix} ] $|$ ``\textbf{\_}'' \\
-  \textit{expr}  & ::= 
-  & \textit{renamed-expr} ( ``\textbf{+}'' \textit{renamed-expr} )$^*$ \\
-  \textit{renamed-expr} & ::=
-  & ( \textit{qualified-name} $|$
-    ``\textbf{(}'' \textit{expr} ``\textbf{)}'' ) \textit{rename}$^*$ \\[2ex]
+  \textit{pos-insts} & ::=
+  & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\
+  \textit{named-insts} & ::=
+  & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term}
+  ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
+  \textit{instance} & ::=
+  & [ \textit{qualifier} \textbf{:} ]
+    \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
+  \textit{expression}  & ::= 
+  & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
+    [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
 
   \multicolumn{3}{l}{Declaration of Locales} \\
 
   \textit{locale} & ::=
   & \textit{element}$^+$ \\
-  & | & \textit{locale-expr} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
+  & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
   \textit{toplevel} & ::=
   & \textbf{locale} \textit{name} [ ``\textbf{=}''
     \textit{locale} ] \\[2ex]
@@ -802,19 +808,17 @@
 
   \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ]
     \textit{prop} \\
-  \textit{insts} & ::= & [ ``\textbf{[}'' \textit{term}$^+$
-    ``\textbf{]}'' ] \\
-  & & [ \textbf{where} \textit{equation} ( \textbf{and}
-    \textit{equation} )$^*$ ] \\
+  \textit{equations} & ::= &  \textbf{where} \textit{equation} ( \textbf{and}
+    \textit{equation} )$^*$  \\
   \textit{toplevel} & ::=
-  & \textbf{interpretation} \textit{name} ( ``$<$'' $|$
-    ``$\subseteq$'' ) \textit{expr} \textit{proof} \\
+  & \textbf{sublocale} \textit{name} ( ``$<$'' $|$
+    ``$\subseteq$'' ) \textit{expression} \textit{proof} \\
   & |
-  & \textbf{interpretation} [ \textit{attr-name} ``\textbf{:}'' ]
-    \textit{expr} \textit{insts} \textit{proof} \\
+  & \textbf{interpretation}
+    \textit{expression} [ \textit{equations} ] \textit{proof} \\
   & |
-  & \textbf{interpret} [ \textit{attr-name} ``\textbf{:}'' ]
-    \textit{expr} \textit{insts} \textit{proof} \\[2ex]
+  & \textbf{interpret}
+    \textit{expression} \textit{proof} \\[2ex]
 
   \multicolumn{3}{l}{Diagnostics} \\
 
@@ -824,7 +828,7 @@
 \end{tabular}
 \end{center}
 \hrule
-\caption{Syntax of Locale Commands.}
+\caption{Syntax of Locale Commands (abrigded).}
 \label{tab:commands}
 \end{table}%
 \end{isamarkuptext}%
diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/document/root.tex
--- a/doc-src/Locales/Locales/document/root.tex	Tue Dec 30 16:50:46 2008 +0100
+++ b/doc-src/Locales/Locales/document/root.tex	Mon Jan 19 20:37:08 2009 +0100
@@ -22,14 +22,17 @@
 
 \begin{document}
 
-\title{Tutorial to Locales and Locale Interpretation}
+\title{Tutorial to Locales and Locale Interpretation \\[1ex]
+  \large 2nd revision, for Isabelle 2009}
 \author{Clemens Ballarin}
 \date{}
 
 \maketitle
 
+%\thispagestyle{myheadings}
+%\markright{Technical Report TUM-I0723, Technische Universit\"at M\"unchen, 2007}
 \thispagestyle{myheadings}
-\markright{Technical Report TUM-I0723, Technische Universit\"at M\"unchen, 2007}
+\markright{This tutorial is currently not consistent.}
 
 \begin{abstract}
   Locales are Isabelle's mechanism to deal with parametric theories.
@@ -40,6 +43,10 @@
 
   This tutorial is intended for locale novices; familiarity with
   Isabelle and Isar is presumed.
+  The 2nd revision accommodates changes introduced by the locales
+  reimplementation for Isabelle 2009.  Most notably, in complex
+  specifications (\emph{locale expressions}) renaming has been
+  generalised to instantiation.
 \end{abstract}
 
 \parindent 0pt\parskip 0.5ex