--- a/doc-src/Locales/Locales/Examples.thy Fri Mar 09 22:05:15 2012 +0100
+++ b/doc-src/Locales/Locales/Examples.thy Sat Mar 10 16:49:34 2012 +0100
@@ -193,7 +193,8 @@
notions of infimum and supremum for partial orders are introduced,
together with theorems about their uniqueness. *}
- context partial_order begin
+ context partial_order
+ begin
definition
is_inf where "is_inf x y i =
--- a/doc-src/Locales/Locales/Examples3.thy Fri Mar 09 22:05:15 2012 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy Sat Mar 10 16:49:34 2012 +0100
@@ -10,8 +10,8 @@
discharge the premise in the definition of @{text "op \<sqsubset>"}. In
general, proofs of the equations not only may involve definitions
from the interpreted locale but arbitrarily complex arguments in the
- context of the locale. Therefore is would be convenient to have the
- interpreted locale conclusions temporary available in the proof.
+ context of the locale. Therefore it would be convenient to have the
+ interpreted locale conclusions temporarily available in the proof.
This can be achieved by a locale interpretation in the proof body.
The command for local interpretations is \isakeyword{interpret}. We
repeat the example from the previous section to illustrate this. *}
@@ -304,7 +304,8 @@
second lattice.
*}
- context lattice_hom begin
+ context lattice_hom
+ begin
abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
abbreviation join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
end
@@ -369,7 +370,8 @@
preserving. As the final example of this section, a locale
interpretation is used to assert this: *}
- sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales
+ sublocale lattice_hom \<subseteq> order_preserving
+ proof unfold_locales
fix x y
assume "x \<sqsubseteq> y"
then have "y = (x \<squnion> y)" by (simp add: le.join_connection)
@@ -481,7 +483,7 @@
locale fun_lattice = fun_partial_order + lattice
sublocale fun_lattice \<subseteq> f: lattice "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
- proof unfold_locales
+ proof unfold_locales
fix f g
have "partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<sqinter> g x)"
apply (rule is_infI) apply rule+ apply (drule spec, assumption)+ done
--- a/doc-src/Locales/Locales/document/Examples.tex Fri Mar 09 22:05:15 2012 +0100
+++ b/doc-src/Locales/Locales/document/Examples.tex Sat Mar 10 16:49:34 2012 +0100
@@ -253,7 +253,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{context}\isamarkupfalse%
-\ partial{\isaliteral{5F}{\isacharunderscore}}order\ \isakeyword{begin}\isanewline
+\ partial{\isaliteral{5F}{\isacharunderscore}}order\isanewline
+\ \ \isakeyword{begin}\isanewline
\isanewline
\ \ \isacommand{definition}\isamarkupfalse%
\isanewline
--- a/doc-src/Locales/Locales/document/Examples3.tex Fri Mar 09 22:05:15 2012 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex Sat Mar 10 16:49:34 2012 +0100
@@ -34,8 +34,8 @@
discharge the premise in the definition of \isa{op\ {\isaliteral{5C3C73717375627365743E}{\isasymsqsubset}}}. In
general, proofs of the equations not only may involve definitions
from the interpreted locale but arbitrarily complex arguments in the
- context of the locale. Therefore is would be convenient to have the
- interpreted locale conclusions temporary available in the proof.
+ context of the locale. Therefore it would be convenient to have the
+ interpreted locale conclusions temporarily available in the proof.
This can be achieved by a locale interpretation in the proof body.
The command for local interpretations is \isakeyword{interpret}. We
repeat the example from the previous section to illustrate this.%
@@ -439,7 +439,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{context}\isamarkupfalse%
-\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\ \isakeyword{begin}\isanewline
+\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\isanewline
+\ \ \isakeyword{begin}\isanewline
\ \ \isacommand{abbreviation}\isamarkupfalse%
\ meet{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7371696E7465723E}{\isasymsqinter}}{\isaliteral{27}{\isacharprime}}{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}meet{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ le{\isaliteral{27}{\isacharprime}}{\isaliteral{2E}{\isachardot}}meet{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{abbreviation}\isamarkupfalse%
@@ -513,9 +514,10 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{sublocale}\isamarkupfalse%
-\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ order{\isaliteral{5F}{\isacharunderscore}}preserving%
+\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ order{\isaliteral{5F}{\isacharunderscore}}preserving\isanewline
+%
\isadelimproof
-\ %
+\ \ %
\endisadelimproof
%
\isatagproof
@@ -738,7 +740,7 @@
\ fun{\isaliteral{5F}{\isacharunderscore}}lattice\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ f{\isaliteral{3A}{\isacharcolon}}\ lattice\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}f\ g{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ g\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
-\ \ \ \ %
+\ \ %
\endisadelimproof
%
\isatagproof