# HG changeset patch
# User ballarin
# Date 1258824353 -3600
# Node ID a3166a169793599c304c49f5b3f67c4ce98684a8
# Parent  a406f447abef0380000a35da0bb0024a3edcacad
Publication details and minor correction of the text.

diff -r a406f447abef -r a3166a169793 doc-src/Locales/Locales/Examples.thy
--- 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
diff -r a406f447abef -r a3166a169793 doc-src/Locales/Locales/document/Examples.tex
--- 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
 \[
diff -r a406f447abef -r a3166a169793 doc-src/Locales/Locales/document/root.tex
--- 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{}