# HG changeset patch
# User immler@in.tum.de
# Date 1232471425 -3600
# Node ID cf1289d989026378a796e599b9f8ca6f79d9ff10
# Parent  479a2fce65e6249108d7bdd5bdbc8b3303c0b71b# Parent  ba144750086d4424c371b795c681adcb51dcb67b
merged

diff -r 479a2fce65e6 -r cf1289d98902 doc-src/Locales/Locales/Examples.thy
--- a/doc-src/Locales/Locales/Examples.thy	Tue Jan 20 16:05:57 2009 +0100
+++ b/doc-src/Locales/Locales/Examples.thy	Tue Jan 20 18:10:25 2009 +0100
@@ -608,7 +608,7 @@
   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. *}
 
   sublocale %visible total_order \<subseteq> lattice
 
diff -r 479a2fce65e6 -r cf1289d98902 doc-src/Locales/Locales/Examples3.thy
--- a/doc-src/Locales/Locales/Examples3.thy	Tue Jan 20 16:05:57 2009 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy	Tue Jan 20 18:10:25 2009 +0100
@@ -178,8 +178,6 @@
   nat_dvd_join_eq} are named since they are handy in the proof of
   the subsequent interpretation. *}
 
-ML %invisible {* set quick_and_dirty *}
-
 (*
 definition
   is_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
@@ -200,8 +198,6 @@
 lemma %invisible gcd_lcm_distr:
   "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry
 
-ML %invisible {* reset quick_and_dirty *}
-  
 interpretation %visible nat_dvd:
   distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   apply unfold_locales
@@ -262,7 +258,7 @@
   preserving maps can be declared in the following way.  *}
 
   locale order_preserving =
-    partial_order + po': partial_order le' for 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"
 
@@ -288,8 +284,7 @@
   obtained by appending the conclusions of the left locale and of the
   right locale.  *}
 
-text {* % FIXME needs update
-  The locale @{text order_preserving} contains theorems for both
+text {* The locale @{text order_preserving} contains theorems for both
   orders @{text \<sqsubseteq>} and @{text \<preceq>}.  How can one refer to a theorem for
   a particular order, @{text \<sqsubseteq>} or @{text \<preceq>}?  Names in locales are
   qualified by the locale parameters.  More precisely, a name is
@@ -298,8 +293,8 @@
 
 context %invisible order_preserving begin
 
-text {* % FIXME needs update?
-  @{thm [source] less_le_trans}: @{thm less_le_trans}
+text {*
+  @{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
 
   @{thm [source] hom_le}: @{thm hom_le}
   *}
@@ -307,12 +302,11 @@
 text {* When renaming a locale, the morphism is also applied
   to the qualifiers.  Hence theorems for the partial order @{text \<preceq>}
   are qualified by @{text le'}.  For example, @{thm [source]
-  po'.less_le_trans}: @{thm [display, indent=2] po'.less_le_trans} *}
+  le'.less_le_trans}: @{thm [display, indent=2] le'.less_le_trans} *}
 
 end %invisible
 
-text {* % FIXME needs update?
-  This example reveals that there is no infix syntax for the strict
+text {* This example reveals that there is no infix syntax for the strict
   version of @{text \<preceq>}!  This can, of course, not be introduced
   automatically, but it can be declared manually through an abbreviation.
   *}
@@ -321,7 +315,7 @@
     less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
 
 text {* Now the theorem is displayed nicely as
-  @{thm [locale=order_preserving] po'.less_le_trans}.  *}
+  @{thm [locale=order_preserving] le'.less_le_trans}.  *}
 
 text {* Not only names of theorems are qualified.  In fact, all names
   are qualified, in particular names introduced by definitions and
@@ -333,7 +327,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 + lat'!: lattice le' for 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)"
@@ -341,9 +335,9 @@
 	"\<phi> (lattice.join le x y) = lattice.join le' (\<phi> x) (\<phi> y)"
 
   abbreviation (in lattice_hom)
-    meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> lat'.meet"
+    meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
   abbreviation (in lattice_hom)
-    join' (infixl "\<squnion>''" 50) where "join' \<equiv> lat'.join"
+    join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
 
 text {* A homomorphism is an endomorphism if both orders coincide. *}
 
@@ -400,17 +394,17 @@
   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: join_connection)
+    then have "y = (x \<squnion> y)" by (simp add: le.join_connection)
     then have "\<phi> y = (\<phi> x \<squnion>' \<phi> y)" by (simp add: hom_join [symmetric])
-    then show "\<phi> x \<preceq> \<phi> y" by (simp add: lat'.join_connection)
+    then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection)
   qed
 
 text {* Theorems and other declarations --- syntax, in particular ---
   from the locale @{text order_preserving} are now active in @{text
   lattice_hom}, for example
 
-  @{thm [locale=lattice_hom, source] lat'.less_le_trans}:
-  @{thm [locale=lattice_hom] lat'.less_le_trans}
+  @{thm [locale=lattice_hom, source] le'.less_le_trans}:
+  @{thm [locale=lattice_hom] le'.less_le_trans}
   *}
 
 
@@ -450,7 +444,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} \\
 
@@ -490,19 +486,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]
@@ -511,19 +511,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} \\
 
@@ -533,7 +531,7 @@
 \end{tabular}
 \end{center}
 \hrule
-\caption{Syntax of Locale Commands.}
+\caption{Syntax of Locale Commands (abridged).}
 \label{tab:commands}
 \end{table}
   *}
diff -r 479a2fce65e6 -r cf1289d98902 doc-src/Locales/Locales/ROOT.ML
--- a/doc-src/Locales/Locales/ROOT.ML	Tue Jan 20 16:05:57 2009 +0100
+++ b/doc-src/Locales/Locales/ROOT.ML	Tue Jan 20 18:10:25 2009 +0100
@@ -1,4 +1,4 @@
 no_document use_thy "GCD";
 use_thy "Examples1";
 use_thy "Examples2";
-use_thy "Examples3";
+setmp_noncritical quick_and_dirty true use_thy "Examples3";
diff -r 479a2fce65e6 -r cf1289d98902 doc-src/Locales/Locales/document/Examples.tex
--- a/doc-src/Locales/Locales/document/Examples.tex	Tue Jan 20 16:05:57 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples.tex	Tue Jan 20 18:10:25 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%
 %
diff -r 479a2fce65e6 -r cf1289d98902 doc-src/Locales/Locales/document/Examples3.tex
--- a/doc-src/Locales/Locales/document/Examples3.tex	Tue Jan 20 16:05:57 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Tue Jan 20 18:10:25 2009 +0100
@@ -362,18 +362,10 @@
 \endisadeliminvisible
 %
 \isataginvisible
-\isacommand{ML}\isamarkupfalse%
-\ {\isacharverbatimopen}\ set\ quick{\isacharunderscore}and{\isacharunderscore}dirty\ {\isacharverbatimclose}\isanewline
-\isanewline
-\isanewline
-\isanewline
 \isacommand{lemma}\isamarkupfalse%
 \ gcd{\isacharunderscore}lcm{\isacharunderscore}distr{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}gcd\ x\ {\isacharparenleft}lcm\ y\ z{\isacharparenright}\ {\isacharequal}\ lcm\ {\isacharparenleft}gcd\ x\ y{\isacharparenright}\ {\isacharparenleft}gcd\ x\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{ML}\isamarkupfalse%
-\ {\isacharverbatimopen}\ reset\ quick{\isacharunderscore}and{\isacharunderscore}dirty\ {\isacharverbatimclose}%
+%
 \endisataginvisible
 {\isafoldinvisible}%
 %
@@ -383,7 +375,7 @@
 \isanewline
 %
 \isadelimvisible
-\ \ \isanewline
+\isanewline
 %
 \endisadelimvisible
 %
@@ -476,7 +468,7 @@
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
 \ order{\isacharunderscore}preserving\ {\isacharequal}\isanewline
-\ \ \ \ partial{\isacharunderscore}order\ {\isacharplus}\ po{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\ \isakeyword{for}\ 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}%
@@ -505,8 +497,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-% FIXME needs update
-  The locale \isa{order{\isacharunderscore}preserving} contains theorems for both
+The locale \isa{order{\isacharunderscore}preserving} contains theorems for both
   orders \isa{{\isasymsqsubseteq}} and \isa{{\isasympreceq}}.  How can one refer to a theorem for
   a particular order, \isa{{\isasymsqsubseteq}} or \isa{{\isasympreceq}}?  Names in locales are
   qualified by the locale parameters.  More precisely, a name is
@@ -530,8 +521,7 @@
 \endisadeliminvisible
 %
 \begin{isamarkuptext}%
-% FIXME needs update?
-  \isa{less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z}
+\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{hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}%
 \end{isamarkuptext}%
@@ -540,7 +530,7 @@
 \begin{isamarkuptext}%
 When renaming a locale, the morphism is also applied
   to the qualifiers.  Hence theorems for the partial order \isa{{\isasympreceq}}
-  are qualified by \isa{le{\isacharprime}}.  For example, \isa{po{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}%
+  are qualified by \isa{le{\isacharprime}}.  For example, \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}%
 \ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\isanewline
 \isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z%
 \end{isabelle}%
@@ -562,8 +552,7 @@
 \endisadeliminvisible
 %
 \begin{isamarkuptext}%
-% FIXME needs update?
-  This example reveals that there is no infix syntax for the strict
+This example reveals that there is no infix syntax for the strict
   version of \isa{{\isasympreceq}}!  This can, of course, not be introduced
   automatically, but it can be declared manually through an abbreviation.%
 \end{isamarkuptext}%
@@ -592,7 +581,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
-\ lattice{\isacharunderscore}hom\ {\isacharequal}\ lattice\ {\isacharplus}\ lat{\isacharprime}{\isacharbang}{\isacharcolon}\ lattice\ le{\isacharprime}\ \isakeyword{for}\ 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
@@ -601,10 +590,10 @@
 \isanewline
 \ \ \isacommand{abbreviation}\isamarkupfalse%
 \ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline
-\ \ \ \ meet{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}meet{\isacharprime}\ {\isasymequiv}\ lat{\isacharprime}{\isachardot}meet{\isachardoublequoteclose}\isanewline
+\ \ \ \ meet{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}meet{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}meet{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{abbreviation}\isamarkupfalse%
 \ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline
-\ \ \ \ join{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}join{\isacharprime}\ {\isasymequiv}\ lat{\isacharprime}{\isachardot}join{\isachardoublequoteclose}%
+\ \ \ \ join{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}join{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}join{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 A homomorphism is an endomorphism if both orders coincide.%
 \end{isamarkuptext}%
@@ -678,7 +667,7 @@
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}y\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ join{\isacharunderscore}connection{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ le{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isasymphi}\ y\ {\isacharequal}\ {\isacharparenleft}{\isasymphi}\ x\ {\isasymsqunion}{\isacharprime}\ {\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
@@ -686,7 +675,7 @@
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ lat{\isacharprime}{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharprime}{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline
 \ \ \isacommand{qed}\isamarkupfalse%
 %
 \endisatagproof
@@ -700,7 +689,7 @@
 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{lat{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
+  \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}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -744,7 +733,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} \\
 
@@ -784,19 +775,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]
@@ -805,19 +800,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} \\
 
@@ -827,7 +820,7 @@
 \end{tabular}
 \end{center}
 \hrule
-\caption{Syntax of Locale Commands.}
+\caption{Syntax of Locale Commands (abridged).}
 \label{tab:commands}
 \end{table}%
 \end{isamarkuptext}%
diff -r 479a2fce65e6 -r cf1289d98902 doc-src/Locales/Locales/document/root.tex
--- a/doc-src/Locales/Locales/document/root.tex	Tue Jan 20 16:05:57 2009 +0100
+++ b/doc-src/Locales/Locales/document/root.tex	Tue Jan 20 18:10:25 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