Update explanation of locale expressions to locale reimplementation.
--- a/doc-src/Locales/Locales/Examples3.thy Fri Mar 27 20:25:07 2009 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy Fri Mar 27 23:43:48 2009 +0100
@@ -250,47 +250,45 @@
Inspecting the grammar of locale commands in
Table~\ref{tab:commands} reveals that the import of a locale can be
more than just a single locale. In general, the import is a
- \emph{locale expression}. Locale expressions enable to combine locales
- and rename parameters. A locale name is a locale expression. If
- $e_1$ and $e_2$ are locale expressions then $e_1 + e_2$ is their
- \emph{merge}. If $e$ is an expression, then $e~q_1 \ldots q_n$ is
- a \emph{renamed expression} where the parameters in $e$ are renamed
- to $q_1 \ldots q_n$. Using a locale expression, a locale for order
+ \emph{locale expression}. These enable to combine locales
+ and instantiate parameters. A locale expression is a sequence of
+ locale \emph{instances} followed by an optional \isakeyword{for}
+ clause. Each instance consists of a locale reference, which may be
+ preceded by a qualifer and succeeded by instantiations of the
+ parameters of that locale. Instantiations may be either positional
+ or through explicit parameter argument pairs.
+
+ Using a locale expression, a locale for order
preserving maps can be declared in the following way. *}
locale order_preserving =
- le: partial_order + le': partial_order le' for le' (infixl "\<preceq>" 50) +
+ le: partial_order le + le': partial_order le'
+ for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) +
fixes \<phi> :: "'a \<Rightarrow> 'b"
assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y"
-text {* The second line contains the expression, which is the
- merge of two partial order locales. The parameter of the second one
- is @{text le'} with new infix syntax @{text \<preceq>}. The
- parameters of the entire locale are @{text le}, @{text le'} and
- @{text \<phi>}. This is their \emph{canonical order},
- which is obtained by a left-to-right traversal of the expression,
- where only the new parameters are appended to the end of the list. The
- parameters introduced in the locale elements of the declaration
- follow.
+text {* The second and third line contain the expression --- two
+ instances of the partial order locale with instantiations @{text le}
+ and @{text le'}, respectively. The \isakeyword{for} clause consists
+ of parameter declarations and is similar to the context element
+ \isakeyword{fixes}. The notable difference is that the
+ \isakeyword{for} clause is part of the expression, and only
+ parameters defined in the expression may occur in its instances.
- In renamings parameters are referred to by position in the canonical
- order; an underscore is used to skip a parameter position, which is
- then not renamed. Renaming deletes the syntax of a parameter unless
- a new mixfix annotation is given.
+ Instances are \emph{morphisms} on locales. Their effect on the
+ parameters is naturally lifted to terms, propositions and theorems,
+ and thus to the assumptions and conclusions of a locale. The
+ assumption of a locale expression is the conjunction of the
+ assumptions of the instances. The conclusions of a sequence of
+ instances are obtained by appending the conclusions of the
+ instances in the order of the sequence.
- Parameter renamings are morphisms between locales. These can be
- lifted to terms and theorems and thus be applied to assumptions and
- conclusions. The assumption of a merge is the conjunction of the
- assumptions of the merged locale. The conclusions of a merge are
- obtained by appending the conclusions of the left locale and of the
- right locale. *}
-
-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
- qualified by the parameters of the locale in which its declaration
- occurs. Here are examples: *}
+ The qualifiers in the expression are already a familiar concept from
+ the \isakeyword{interpretation} command. They serve to distinguish
+ names (in particular theorem names) for the two partial orders
+ within the locale. Qualifiers in the \isakeyword{locale} command
+ default to optional. Here are examples of theorems in locale @{text
+ order_preserving}: *}
context %invisible order_preserving begin
@@ -300,16 +298,14 @@
@{thm [source] hom_le}: @{thm hom_le}
*}
-text {* When renaming a locale, the morphism is also applied
- to the qualifiers. Hence theorems for the partial order @{text \<preceq>}
+text {* The theorems for the partial order @{text \<preceq>}
are qualified by @{text le'}. For example, @{thm [source]
le'.less_le_trans}: @{thm [display, indent=2] le'.less_le_trans} *}
end %invisible
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.
+ version of @{text \<preceq>}! This can be declared through an abbreviation.
*}
abbreviation (in order_preserving)
@@ -318,22 +314,39 @@
text (in order_preserving) {* Now the theorem is displayed nicely as
@{thm 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
- abbreviations. The name of the strict order of @{text \<sqsubseteq>} is @{text
- le.less} and therefore @{text le'.less} is the name of the strict
- order of @{text \<preceq>}. Hence, the equation in the above abbreviation
- could have been written as @{text "less' \<equiv> le'.less"}. *}
+text {* Qualifiers not only apply to theorem names, but also to names
+ introduced by definitions and abbreviations. In locale
+ @{text partial_order} the full name of the strict order of @{text \<sqsubseteq>} is
+ @{text le.less} and therefore @{text le'.less} is the full name of
+ the strict order of @{text \<preceq>}. Hence, the equation in the
+ abbreviation above could have been also written as @{text "less' \<equiv>
+ le'.less"}. *}
-text {* Two more locales illustrate working with locale expressions.
- A map @{text \<phi>} is a lattice homomorphism if it preserves meet and join. *}
+text {* Readers may find the declaration of locale @{text
+ order_preserving} a little awkward, because the declaration and
+ concrete syntax for @{text le} from @{text partial_order} are
+ repeated in the declaration of @{text order_preserving}. Locale
+ expressions provide a convenient short hand for this. A parameter
+ in an instance is \emph{untouched} if no instantiation term is
+ provided for it. In positional instantiations, a parameter position
+ may be skipped with an underscore, and it is allowed to give fewer
+ instantiation terms than the instantiated locale's number of
+ parameters. In named instantiations, instantiation pairs for
+ certain parameters may simply be omitted. Untouched parameters are
+ declared by the locale expression and with their concrete syntax by
+ implicitly adding them to the beginning of the \isakeyword{for}
+ clause.
- locale lattice_hom = le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
+ The following locales illustrate this. A map @{text \<phi>} is a
+ lattice homomorphism if it preserves meet and join. *}
+
+ 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)"
+ "\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)"
and hom_join:
- "\<phi> (lattice.join le x y) = lattice.join le' (\<phi> x) (\<phi> y)"
+ "\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)"
abbreviation (in lattice_hom)
meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
@@ -342,8 +355,12 @@
text {* A homomorphism is an endomorphism if both orders coincide. *}
- locale lattice_end =
- lattice_hom le le for le (infixl "\<sqsubseteq>" 50)
+ locale lattice_end = lattice_hom _ le
+
+text {* In this declaration, the first parameter of @{text
+ lattice_hom}, @{text le}, is untouched and then used to instantiate
+ the second parameter. Its concrete syntax is preseverd. *}
+
text {* The inheritance diagram of the situation we have now is shown
in Figure~\ref{fig:hom}, where the dashed line depicts an
@@ -390,7 +407,7 @@
text {* It can be shown easily that a lattice homomorphism is order
preserving. As the final example of this section, a locale
- interpretation is used to assert this. *}
+ interpretation is used to assert this: *}
sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales
fix x y
@@ -404,6 +421,7 @@
Theorems and other declarations --- syntax, in particular --- from
the locale @{text order_preserving} are now active in @{text
lattice_hom}, for example
+
@{thm [source] le'.less_le_trans}:
@{thm le'.less_le_trans}
*}
@@ -423,7 +441,7 @@
Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction
of axiomatic type classes through a combination with locale
interpretation. The result is a Haskell-style class system with a
- facility to generate Haskell code. Classes are sufficient for
+ facility to generate ML and Haskell code. Classes are sufficient for
simple specifications with a single type parameter. The locales for
orders and lattices presented in this tutorial fall into this
category. Order preserving maps, homomorphisms and vector spaces,
--- a/doc-src/Locales/Locales/document/Examples3.tex Fri Mar 27 20:25:07 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex Fri Mar 27 23:43:48 2009 +0100
@@ -457,52 +457,46 @@
Inspecting the grammar of locale commands in
Table~\ref{tab:commands} reveals that the import of a locale can be
more than just a single locale. In general, the import is a
- \emph{locale expression}. Locale expressions enable to combine locales
- and rename parameters. A locale name is a locale expression. If
- $e_1$ and $e_2$ are locale expressions then $e_1 + e_2$ is their
- \emph{merge}. If $e$ is an expression, then $e~q_1 \ldots q_n$ is
- a \emph{renamed expression} where the parameters in $e$ are renamed
- to $q_1 \ldots q_n$. Using a locale expression, a locale for order
+ \emph{locale expression}. These enable to combine locales
+ and instantiate parameters. A locale expression is a sequence of
+ locale \emph{instances} followed by an optional \isakeyword{for}
+ clause. Each instance consists of a locale reference, which may be
+ preceded by a qualifer and succeeded by instantiations of the
+ parameters of that locale. Instantiations may be either positional
+ or through explicit parameter argument pairs.
+
+ Using a locale expression, a locale for order
preserving maps can be declared in the following way.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{locale}\isamarkupfalse%
\ order{\isacharunderscore}preserving\ {\isacharequal}\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
+\ \ \ \ le{\isacharcolon}\ partial{\isacharunderscore}order\ le\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\isanewline
+\ \ \ \ \ \ \isakeyword{for}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{and}\ 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}%
-The second line contains the expression, which is the
- merge of two partial order locales. The parameter of the second one
- is \isa{le{\isacharprime}} with new infix syntax \isa{{\isasympreceq}}. The
- parameters of the entire locale are \isa{le}, \isa{le{\isacharprime}} and
- \isa{{\isasymphi}}. This is their \emph{canonical order},
- which is obtained by a left-to-right traversal of the expression,
- where only the new parameters are appended to the end of the list. The
- parameters introduced in the locale elements of the declaration
- follow.
-
- In renamings parameters are referred to by position in the canonical
- order; an underscore is used to skip a parameter position, which is
- then not renamed. Renaming deletes the syntax of a parameter unless
- a new mixfix annotation is given.
+The second and third line contain the expression --- two
+ instances of the partial order locale with instantiations \isa{le}
+ and \isa{le{\isacharprime}}, respectively. The \isakeyword{for} clause consists
+ of parameter declarations and is similar to the context element
+ \isakeyword{fixes}. The notable difference is that the
+ \isakeyword{for} clause is part of the expression, and only
+ parameters defined in the expression may occur in its instances.
- Parameter renamings are morphisms between locales. These can be
- lifted to terms and theorems and thus be applied to assumptions and
- conclusions. The assumption of a merge is the conjunction of the
- assumptions of the merged locale. The conclusions of a merge are
- obtained by appending the conclusions of the left locale and of the
- right locale.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-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
- qualified by the parameters of the locale in which its declaration
- occurs. Here are examples:%
+ Instances are \emph{morphisms} on locales. Their effect on the
+ parameters is naturally lifted to terms, propositions and theorems,
+ and thus to the assumptions and conclusions of a locale. The
+ assumption of a locale expression is the conjunction of the
+ assumptions of the instances. The conclusions of a sequence of
+ instances are obtained by appending the conclusions of the
+ instances in the order of the sequence.
+
+ The qualifiers in the expression are already a familiar concept from
+ the \isakeyword{interpretation} command. They serve to distinguish
+ names (in particular theorem names) for the two partial orders
+ within the locale. Qualifiers in the \isakeyword{locale} command
+ default to optional. Here are examples of theorems in locale \isa{order{\isacharunderscore}preserving}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -528,8 +522,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-When renaming a locale, the morphism is also applied
- to the qualifiers. Hence theorems for the partial order \isa{{\isasympreceq}}
+The theorems for the partial order \isa{{\isasympreceq}}
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%
@@ -553,8 +546,7 @@
%
\begin{isamarkuptext}%
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.%
+ version of \isa{{\isasympreceq}}! This can be declared through an abbreviation.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{abbreviation}\isamarkupfalse%
@@ -567,26 +559,42 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Not only names of theorems are qualified. In fact, all names
- are qualified, in particular names introduced by definitions and
- abbreviations. The name of the strict order of \isa{{\isasymsqsubseteq}} is \isa{le{\isachardot}less} and therefore \isa{le{\isacharprime}{\isachardot}less} is the name of the strict
- order of \isa{{\isasympreceq}}. Hence, the equation in the above abbreviation
- could have been written as \isa{less{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}less}.%
+Qualifiers not only apply to theorem names, but also to names
+ introduced by definitions and abbreviations. In locale
+ \isa{partial{\isacharunderscore}order} the full name of the strict order of \isa{{\isasymsqsubseteq}} is
+ \isa{le{\isachardot}less} and therefore \isa{le{\isacharprime}{\isachardot}less} is the full name of
+ the strict order of \isa{{\isasympreceq}}. Hence, the equation in the
+ abbreviation above could have been also written as \isa{less{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}less}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Two more locales illustrate working with locale expressions.
- A map \isa{{\isasymphi}} is a lattice homomorphism if it preserves meet and join.%
+Readers may find the declaration of locale \isa{order{\isacharunderscore}preserving} a little awkward, because the declaration and
+ concrete syntax for \isa{le} from \isa{partial{\isacharunderscore}order} are
+ repeated in the declaration of \isa{order{\isacharunderscore}preserving}. Locale
+ expressions provide a convenient short hand for this. A parameter
+ in an instance is \emph{untouched} if no instantiation term is
+ provided for it. In positional instantiations, a parameter position
+ may be skipped with an underscore, and it is allowed to give fewer
+ instantiation terms than the instantiated locale's number of
+ parameters. In named instantiations, instantiation pairs for
+ certain parameters may simply be omitted. Untouched parameters are
+ declared by the locale expression and with their concrete syntax by
+ implicitly adding them to the beginning of the \isakeyword{for}
+ clause.
+
+ The following locales illustrate this. A map \isa{{\isasymphi}} is a
+ lattice homomorphism if it preserves meet and join.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{locale}\isamarkupfalse%
-\ 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
+\ lattice{\isacharunderscore}hom\ {\isacharequal}\isanewline
+\ \ \ \ 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
+\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqinter}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}meet\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isakeyword{and}\ hom{\isacharunderscore}join{\isacharcolon}\isanewline
-\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}lattice{\isachardot}join\ le\ x\ y{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}join\ le{\isacharprime}\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}join\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isacommand{abbreviation}\isamarkupfalse%
\ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline
@@ -599,8 +607,13 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{locale}\isamarkupfalse%
-\ lattice{\isacharunderscore}end\ {\isacharequal}\isanewline
-\ \ \ \ lattice{\isacharunderscore}hom\ le\ le\ \isakeyword{for}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
+\ lattice{\isacharunderscore}end\ {\isacharequal}\ lattice{\isacharunderscore}hom\ {\isacharunderscore}\ le%
+\begin{isamarkuptext}%
+In this declaration, the first parameter of \isa{lattice{\isacharunderscore}hom}, \isa{le}, is untouched and then used to instantiate
+ the second parameter. Its concrete syntax is preseverd.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\begin{isamarkuptext}%
The inheritance diagram of the situation we have now is shown
in Figure~\ref{fig:hom}, where the dashed line depicts an
@@ -648,7 +661,7 @@
\begin{isamarkuptext}%
It can be shown easily that a lattice homomorphism is order
preserving. As the final example of this section, a locale
- interpretation is used to assert this.%
+ interpretation is used to assert this:%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{sublocale}\isamarkupfalse%
@@ -688,6 +701,7 @@
\begin{isamarkuptext}%
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{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}%
@@ -709,7 +723,7 @@
Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction
of axiomatic type classes through a combination with locale
interpretation. The result is a Haskell-style class system with a
- facility to generate Haskell code. Classes are sufficient for
+ facility to generate ML and Haskell code. Classes are sufficient for
simple specifications with a single type parameter. The locales for
orders and lattices presented in this tutorial fall into this
category. Order preserving maps, homomorphisms and vector spaces,