author wenzelm Sat, 10 Mar 2012 16:49:34 +0100 changeset 46855 f72a2bedd7a9 parent 46854 940dbfd43dc4 child 46856 28909eecdf5b
more precise alignment of begin/end, proof/qed; improved English;
--- 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%
\ \ \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
+%
-\ %
+\ \ %
\isatagproof