doc-src/IsarRef/pure.tex

 
 \railalias{MLcommand}{ML\_command}
 \railterm{MLcommand}
 
 \begin{rail}
-  'use' name
-  ;
-  ('ML' | MLcommand | MLsetup | 'setup') text
+  'use' name comment?
+  ;
+  ('ML' | MLcommand | MLsetup | 'setup') text comment?
   ;
   methodsetup name '=' text text comment?
   ;
 \end{rail}
 

   \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
   \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
   \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
   \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
 \end{matharray}
+
+\railalias{parseasttranslation}{parse\_ast\_translation}
+\railterm{parseasttranslation}
+
+\railalias{parsetranslation}{parse\_translation}
+\railterm{parsetranslation}
+
+\railalias{printtranslation}{print\_translation}
+\railterm{printtranslation}
+
+\railalias{typedprinttranslation}{typed\_print\_translation}
+\railterm{typedprinttranslation}
+
+\railalias{printasttranslation}{print\_ast\_translation}
+\railterm{printasttranslation}
+
+\railalias{tokentranslation}{token\_translation}
+\railterm{tokentranslation}
+
+\begin{rail}
+  ( parseasttranslation | parsetranslation | printtranslation | typedprinttranslation |
+  printasttranslation | tokentranslation ) text comment?
+\end{rail}
 
 Syntax translation functions written in ML admit almost arbitrary
 manipulations of Isabelle's inner syntax.  Any of the above commands have a
 single \railqtoken{text} argument that refers to an ML expression of
 appropriate type.

   ;
   'defer' nat? comment?
   ;
   'prefer' nat comment?
   ;
+  'back' comment?
+  ;
 \end{rail}
 
 \begin{descr}
 \item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in initial
   position, but unlike $\PROOFNAME$ it retains ``$proof(prove)$'' mode.  Thus