Merged, overriding earlier fix.
--- a/doc-src/Locales/Locales/Examples.thy Mon Jan 19 20:05:41 2009 +0100
+++ b/doc-src/Locales/Locales/Examples.thy Mon Jan 19 21:20:18 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
--- a/doc-src/Locales/Locales/Examples3.thy Mon Jan 19 20:05:41 2009 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy Mon Jan 19 21:20:18 2009 +0100
@@ -262,7 +262,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 +288,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 +297,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 +306,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 +319,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 +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 + 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 +339,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 +398,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 +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} \\
@@ -490,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]
@@ -511,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} \\
@@ -533,7 +535,7 @@
\end{tabular}
\end{center}
\hrule
-\caption{Syntax of Locale Commands.}
+\caption{Syntax of Locale Commands (abridged).}
\label{tab:commands}
\end{table}
*}
--- a/doc-src/Locales/Locales/document/Examples.tex Mon Jan 19 20:05:41 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples.tex Mon Jan 19 21:20:18 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%
%
--- a/doc-src/Locales/Locales/document/Examples3.tex Mon Jan 19 20:05:41 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex Mon Jan 19 21:20:18 2009 +0100
@@ -476,7 +476,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 +505,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 +529,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 +538,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 +560,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 +589,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 +598,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 +675,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 +683,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 +697,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 +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} \\
@@ -784,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]
@@ -805,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} \\
@@ -827,7 +828,7 @@
\end{tabular}
\end{center}
\hrule
-\caption{Syntax of Locale Commands.}
+\caption{Syntax of Locale Commands (abridged).}
\label{tab:commands}
\end{table}%
\end{isamarkuptext}%
--- a/doc-src/Locales/Locales/document/root.tex Mon Jan 19 20:05:41 2009 +0100
+++ b/doc-src/Locales/Locales/document/root.tex Mon Jan 19 21:20:18 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