# HG changeset patch
# User wenzelm
# Date 1212589102 -7200
# Node ID 34005fa42128f945706bd997a9cf0836806bd7a0
# Parent  34f3784d40f2e4a004656459dc4f4f992b0b6f71
renamed expression: plain ~ (space) instead of \colon;

diff -r 34f3784d40f2 -r 34005fa42128 doc-src/Locales/Locales/Examples3.thy
--- a/doc-src/Locales/Locales/Examples3.thy	Wed Jun 04 12:29:33 2008 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy	Wed Jun 04 16:18:22 2008 +0200
@@ -258,7 +258,7 @@
   \emph{locale expression}.  Locale expressions enable to combine locales
   and rename parameters.  A locale name is a locale expression.  If
   $e_1$ and $e_2$ are locale expressions then $e_1 + e_2$ is their
-  \emph{merge}.  If $e$ is an expression, then $e\colon q_1 \ldots q_n$ is
+  \emph{merge}.  If $e$ is an expression, then $e~q_1 \ldots q_n$ is
   a \emph{renamed expression} where the parameters in $e$ are renamed
   to $q_1 \ldots q_n$.  Using a locale expression, a locale for order
   preserving maps can be declared in the following way.  *}
diff -r 34f3784d40f2 -r 34005fa42128 doc-src/Locales/Locales/document/Examples3.tex
--- a/doc-src/Locales/Locales/document/Examples3.tex	Wed Jun 04 12:29:33 2008 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Wed Jun 04 16:18:22 2008 +0200
@@ -462,7 +462,7 @@
   \emph{locale expression}.  Locale expressions enable to combine locales
   and rename parameters.  A locale name is a locale expression.  If
   $e_1$ and $e_2$ are locale expressions then $e_1 + e_2$ is their
-  \emph{merge}.  If $e$ is an expression, then $e\colon q_1 \ldots q_n$ is
+  \emph{merge}.  If $e$ is an expression, then $e~q_1 \ldots q_n$ is
   a \emph{renamed expression} where the parameters in $e$ are renamed
   to $q_1 \ldots q_n$.  Using a locale expression, a locale for order
   preserving maps can be declared in the following way.%