Publication details and minor correction of the text.
--- a/doc-src/Locales/Locales/Examples.thy Sat Nov 21 17:39:54 2009 +0100
+++ b/doc-src/Locales/Locales/Examples.thy Sat Nov 21 18:25:53 2009 +0100
@@ -26,7 +26,7 @@
\[
@{text "\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> \<dots>"}
\]
- where variables~@{text "x\<^sub>1"}, \ldots,~@{text "x\<^sub>n"} are called
+ where the variables~@{text "x\<^sub>1"}, \ldots,~@{text "x\<^sub>n"} are called
\emph{parameters} and the premises $@{text "A\<^sub>1"}, \ldots,~@{text
"A\<^sub>m"}$ \emph{assumptions}. A formula~@{text "C"}
is a \emph{theorem} in the context if it is a conclusion
--- a/doc-src/Locales/Locales/document/Examples.tex Sat Nov 21 17:39:54 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples.tex Sat Nov 21 18:25:53 2009 +0100
@@ -46,7 +46,7 @@
\[
\isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}{\isasymdots}x\isactrlsub n{\isachardot}\ {\isasymlbrakk}\ A\isactrlsub {\isadigit{1}}{\isacharsemicolon}\ {\isasymdots}\ {\isacharsemicolon}A\isactrlsub m\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymdots}}
\]
- where variables~\isa{x\isactrlsub {\isadigit{1}}}, \ldots,~\isa{x\isactrlsub n} are called
+ where the variables~\isa{x\isactrlsub {\isadigit{1}}}, \ldots,~\isa{x\isactrlsub n} are called
\emph{parameters} and the premises $\isa{A\isactrlsub {\isadigit{1}}}, \ldots,~\isa{A\isactrlsub m}$ \emph{assumptions}. A formula~\isa{C}
is a \emph{theorem} in the context if it is a conclusion
\[
--- a/doc-src/Locales/Locales/document/root.tex Sat Nov 21 17:39:54 2009 +0100
+++ b/doc-src/Locales/Locales/document/root.tex Sat Nov 21 18:25:53 2009 +0100
@@ -23,7 +23,8 @@
\begin{document}
-\title{Tutorial to Locales and Locale Interpretation}
+\title{Tutorial to Locales and Locale Interpretation%
+\thanks{Published in L.~Lamb\'an, A.~Romero, J.~Rubio, editors, {\em Contribuciones Cient\'{\i}ficas en honor de Mirian Andr\'es.} Servicio de Publicaciones de la Universidad de La Rioja, Logro\~no, Spain, 2010. Reproduced by permission.}}
\author{Clemens Ballarin}
\date{}