--- a/doc-src/IsarRef/pure.tex Mon Dec 11 20:08:19 2000 +0100
+++ b/doc-src/IsarRef/pure.tex Mon Dec 11 20:09:47 2000 +0100
@@ -267,10 +267,19 @@
\isarcmd{translations} & : & \isartrans{theory}{theory} \\
\end{matharray}
+\railalias{rightleftharpoons}{\isasymrightleftharpoons}
+\railterm{rightleftharpoons}
+
+\railalias{rightharpoonup}{\isasymrightharpoonup}
+\railterm{rightharpoonup}
+
+\railalias{leftharpoondown}{\isasymleftharpoondown}
+\railterm{leftharpoondown}
+
\begin{rail}
'syntax' ('(' ( name | 'output' | name 'output' ) ')')? (constdecl +)
;
- 'translations' (transpat ('==' | '=>' | '<=') transpat comment? +)
+ 'translations' (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat comment? +)
;
transpat: ('(' nameref ')')? string
;
@@ -285,10 +294,11 @@
flag is given, all productions are added both to the input and output
grammar.
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation
- rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==}), parse rules
- (\texttt{=>}), or print rules (\texttt{<=}). Translation patterns may be
- prefixed by the syntactic category to be used for parsing; the default is
- \texttt{logic}.
+ rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==} or
+ \isasymrightleftharpoons), parse rules (\texttt{=>} or
+ \isasymrightharpoonup), or print rules (\texttt{<=} or
+ \isasymleftharpoondown). Translation patterns may be prefixed by the
+ syntactic category to be used for parsing; the default is \texttt{logic}.
\end{descr}