# HG changeset patch
# User wenzelm
# Date 1331394574 -3600
# Node ID f72a2bedd7a90703fbcc17c2045ee8a89a8cd9b5
# Parent  940dbfd43dc4720fcf3a7b6538a0c1aae663215b
more precise alignment of begin/end, proof/qed;
improved English;

diff -r 940dbfd43dc4 -r f72a2bedd7a9 doc-src/Locales/Locales/Examples.thy
--- 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 =
diff -r 940dbfd43dc4 -r f72a2bedd7a9 doc-src/Locales/Locales/Examples3.thy
--- 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
diff -r 940dbfd43dc4 -r f72a2bedd7a9 doc-src/Locales/Locales/document/Examples.tex
--- 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
diff -r 940dbfd43dc4 -r f72a2bedd7a9 doc-src/Locales/Locales/document/Examples3.tex
--- 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