--- a/doc-src/IsarRef/pure.tex Sat Apr 16 18:54:44 2005 +0200
+++ b/doc-src/IsarRef/pure.tex Sat Apr 16 18:55:28 2005 +0200
@@ -295,9 +295,10 @@
\subsection{Syntax and translations}\label{sec:syn-trans}
-\indexisarcmd{syntax}\indexisarcmd{translations}
+\indexisarcmd{syntax}\indexisarcmd{no-syntax}\indexisarcmd{translations}
\begin{matharray}{rcl}
\isarcmd{syntax} & : & \isartrans{theory}{theory} \\
+ \isarcmd{no_syntax} & : & \isartrans{theory}{theory} \\
\isarcmd{translations} & : & \isartrans{theory}{theory} \\
\end{matharray}
@@ -310,11 +311,17 @@
\railalias{leftharpoondown}{\isasymleftharpoondown}
\railterm{leftharpoondown}
+\railalias{nosyntax}{no\_syntax}
+\railterm{nosyntax}
+
\begin{rail}
- 'syntax' ('(' ( name | 'output' | name 'output' ) ')')? (constdecl +)
+ ('syntax' | nosyntax) mode? (constdecl +)
;
'translations' (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
;
+
+ mode: ('(' ( name | 'output' | name 'output' ) ')')
+ ;
transpat: ('(' nameref ')')? string
;
\end{rail}
@@ -329,6 +336,10 @@
$\isarkeyword{output}$ indicator is given, all productions are added both to
the input and output grammar.
+\item [$\isarkeyword{no_syntax}~(mode)~decls$] removes grammar declarations
+ (and translations) resulting from $decls$, which are interpreted in the same
+ manner as for $\isarkeyword{syntax}$ above.
+
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation
rules (i.e.\ macros): parse~/ print rules (\isasymrightleftharpoons), parse
rules (\isasymrightharpoonup), or print rules (\isasymleftharpoondown).