--- 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
--- 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}
*}
--- 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";
--- 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%
%
--- 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}%
--- 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