# 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 \"}. 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 "\''" 50) where "meet' \ le'.meet" abbreviation join' (infixl "\''" 50) where "join' \ 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 \ order_preserving proof unfold_locales + sublocale lattice_hom \ order_preserving + proof unfold_locales fix x y assume "x \ y" then have "y = (x \ y)" by (simp add: le.join_connection) @@ -481,7 +483,7 @@ locale fun_lattice = fun_partial_order + lattice sublocale fun_lattice \ f: lattice "\f g. \x. f x \ g x" - proof unfold_locales + proof unfold_locales fix f g have "partial_order.is_inf (\f g. \x. f x \ g x) f g (\x. f x \ 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