# HG changeset patch
# User ballarin
# Date 1238195462 -3600
# Node ID 36a255c2e42864b979202f260bde54daecd1a4ef
# Parent  3779e2158dad321e12b69eef4cd21a9ca3f45640
Corrections to locale syntax.

diff -r 3779e2158dad -r 36a255c2e428 doc-src/Locales/Locales/Examples3.thy
--- a/doc-src/Locales/Locales/Examples3.thy	Fri Mar 27 23:43:48 2009 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy	Sat Mar 28 00:11:02 2009 +0100
@@ -465,7 +465,7 @@
   & \textit{name} $|$ \textit{attribute} $|$
     \textit{name} \textit{attribute} \\
   \textit{qualifier} & ::=
-  & \textit{name} [``\textbf{!}''] \\[2ex]
+  & \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex]
 
   \multicolumn{3}{l}{Context Elements} \\
 
@@ -511,7 +511,7 @@
   & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term}
   ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
   \textit{instance} & ::=
-  & [ \textit{qualifier} \textbf{:} ]
+  & [ \textit{qualifier} ``\textbf{:}'' ]
     \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
   \textit{expression}  & ::= 
   & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
diff -r 3779e2158dad -r 36a255c2e428 doc-src/Locales/Locales/document/Examples3.tex
--- a/doc-src/Locales/Locales/document/Examples3.tex	Fri Mar 27 23:43:48 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Sat Mar 28 00:11:02 2009 +0100
@@ -748,7 +748,7 @@
   & \textit{name} $|$ \textit{attribute} $|$
     \textit{name} \textit{attribute} \\
   \textit{qualifier} & ::=
-  & \textit{name} [``\textbf{!}''] \\[2ex]
+  & \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex]
 
   \multicolumn{3}{l}{Context Elements} \\
 
@@ -794,7 +794,7 @@
   & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term}
   ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
   \textit{instance} & ::=
-  & [ \textit{qualifier} \textbf{:} ]
+  & [ \textit{qualifier} ``\textbf{:}'' ]
     \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
   \textit{expression}  & ::= 
   & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$