# HG changeset patch
# User wenzelm
# Date 976561787 -3600
# Node ID 562e20e543b10fb283a5774ca846cdab2320b5d4
# Parent  f902346264e90122c6100e09f7b7c5dfb952408c
alternative syntax for "translations": harpoons;

diff -r f902346264e9 -r 562e20e543b1 doc-src/IsarRef/pure.tex
--- 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}