# 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}