# 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} )$^*$