# HG changeset patch # User wenzelm # Date 950709852 -3600 # Node ID f4029c34adef3e4369c6da6bf03e098c0aa6c606 # Parent 3fc32155372c23d892806378e8e35886ed9734ad Syntax translation functions; diff -r 3fc32155372c -r f4029c34adef doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Wed Feb 16 10:51:23 2000 +0100 +++ b/doc-src/IsarRef/pure.tex Wed Feb 16 15:04:12 2000 +0100 @@ -376,26 +376,25 @@ \end{descr} -%FIXME remove!? -%\subsection{Syntax translation functions} +\subsection{Syntax translation functions} -%\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation} -%\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation} -%\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation} -%\begin{matharray}{rcl} -% \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\ -% \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\ -% \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} +\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation} +\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation} +\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation} +\begin{matharray}{rcl} + \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\ + \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\ + \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} -%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. See \cite[\S8]{isabelle-ref} for more information on syntax -%transformations. +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. See \cite[\S8]{isabelle-ref} for more information on syntax +transformations. \subsection{Oracles}