# HG changeset patch # User ballarin # Date 1275247777 -7200 # Node ID 7f2a6f3143adab0dca5c73c59a5ff68941660baf # Parent 2b4e52ecf6fcfdf9fc59aabd25401cd034900ddc Typo in locales tutorial. diff -r 2b4e52ecf6fc -r 7f2a6f3143ad doc-src/Locales/Locales/Examples.thy --- a/doc-src/Locales/Locales/Examples.thy Sat May 29 20:49:04 2010 +0200 +++ b/doc-src/Locales/Locales/Examples.thy Sun May 30 21:29:37 2010 +0200 @@ -107,7 +107,7 @@ in the theory. Technically, this is simply the theorem composed of context and conclusion. For the transitivity theorem, this is @{thm [source] partial_order.trans}: - @{thm [display, indent=2] partial_order_def} + @{thm [display, indent=2] partial_order.trans} *} subsection {* Targets: Extending Locales *} diff -r 2b4e52ecf6fc -r 7f2a6f3143ad doc-src/Locales/Locales/Examples3.thy --- a/doc-src/Locales/Locales/Examples3.thy Sat May 29 20:49:04 2010 +0200 +++ b/doc-src/Locales/Locales/Examples3.thy Sun May 30 21:29:37 2010 +0200 @@ -645,7 +645,8 @@ have been generalised from renaming to instantiation. *} text {* \textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow, - Randy Pollack, Christian Sternagel and Makarius Wenzel have made + Randy Pollack, Andreas Schropp, Christian Sternagel and Makarius Wenzel + have made useful comments on earlier versions of this document. The section on conditional interpretation was inspired by a number of e-mail enquiries the author received from locale users, and which suggested diff -r 2b4e52ecf6fc -r 7f2a6f3143ad doc-src/Locales/Locales/document/Examples.tex --- a/doc-src/Locales/Locales/document/Examples.tex Sat May 29 20:49:04 2010 +0200 +++ b/doc-src/Locales/Locales/document/Examples.tex Sun May 30 21:29:37 2010 +0200 @@ -134,10 +134,7 @@ of context and conclusion. For the transitivity theorem, this is \isa{partial{\isacharunderscore}order{\isachardot}trans}: \begin{isabelle}% -\ \ partial{\isacharunderscore}order\ {\isacharquery}le\ {\isasymequiv}\isanewline -\isaindent{\ \ }{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}le\ x\ x{\isacharparenright}\ {\isasymand}\isanewline -\isaindent{\ \ }{\isacharparenleft}{\isasymforall}x\ y{\isachardot}\ {\isacharquery}le\ x\ y\ {\isasymlongrightarrow}\ {\isacharquery}le\ y\ x\ {\isasymlongrightarrow}\ x\ {\isacharequal}\ y{\isacharparenright}\ {\isasymand}\isanewline -\isaindent{\ \ }{\isacharparenleft}{\isasymforall}x\ y\ z{\isachardot}\ {\isacharquery}le\ x\ y\ {\isasymlongrightarrow}\ {\isacharquery}le\ y\ z\ {\isasymlongrightarrow}\ {\isacharquery}le\ x\ z{\isacharparenright}% +\ \ {\isasymlbrakk}partial{\isacharunderscore}order\ {\isacharquery}le{\isacharsemicolon}\ {\isacharquery}le\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}le\ {\isacharquery}y\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}le\ {\isacharquery}x\ {\isacharquery}z% \end{isabelle}% \end{isamarkuptext}% \isamarkuptrue% @@ -1264,7 +1261,7 @@ definitions and other constructs that are not part of the specifications of the locales. - The first from of interpretation we will consider in this tutorial + The first form of interpretation we will consider in this tutorial is provided by the \isakeyword{sublocale} command. It enables to modify the import hierarchy to reflect the \emph{logical} relation between locales. diff -r 2b4e52ecf6fc -r 7f2a6f3143ad doc-src/Locales/Locales/document/Examples3.tex --- a/doc-src/Locales/Locales/document/Examples3.tex Sat May 29 20:49:04 2010 +0200 +++ b/doc-src/Locales/Locales/document/Examples3.tex Sun May 30 21:29:37 2010 +0200 @@ -941,7 +941,8 @@ % \begin{isamarkuptext}% \textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow, - Randy Pollack, Christian Sternagel and Makarius Wenzel have made + Randy Pollack, Andreas Schropp, Christian Sternagel and Makarius Wenzel + have made useful comments on earlier versions of this document. The section on conditional interpretation was inspired by a number of e-mail enquiries the author received from locale users, and which suggested