# 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