doc-src/IsarRef/pure.tex
changeset 8250 f4029c34adef
parent 8207 985c876b777e
child 8379 4c7659e98eb9
equal deleted inserted replaced
8249:3fc32155372c 8250:f4029c34adef
   374   theory)~list$.  The $\isarkeyword{setup}$ command is the canonical way to
   374   theory)~list$.  The $\isarkeyword{setup}$ command is the canonical way to
   375   initialize object-logic specific tools and packages written in ML.
   375   initialize object-logic specific tools and packages written in ML.
   376 \end{descr}
   376 \end{descr}
   377 
   377 
   378 
   378 
   379 %FIXME remove!?
   379 \subsection{Syntax translation functions}
   380 %\subsection{Syntax translation functions}
   380 
   381 
   381 \indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
   382 %\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
   382 \indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
   383 %\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
   383 \indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
   384 %\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
   384 \begin{matharray}{rcl}
   385 %\begin{matharray}{rcl}
   385   \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
   386 %  \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
   386   \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
   387 %  \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
   387   \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
   388 %  \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
   388   \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
   389 %  \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
   389   \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
   390 %  \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
   390   \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
   391 %  \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
   391 \end{matharray}
   392 %\end{matharray}
   392 
   393 
   393 Syntax translation functions written in ML admit almost arbitrary
   394 %Syntax translation functions written in ML admit almost arbitrary
   394 manipulations of Isabelle's inner syntax.  Any of the above commands have a
   395 %manipulations of Isabelle's inner syntax.  Any of the above commands have a
   395 single \railqtoken{text} argument that refers to an ML expression of
   396 %single \railqtoken{text} argument that refers to an ML expression of
   396 appropriate type.  See \cite[\S8]{isabelle-ref} for more information on syntax
   397 %appropriate type.  See \cite[\S8]{isabelle-ref} for more information on syntax
   397 transformations.
   398 %transformations.
       
   399 
   398 
   400 
   399 
   401 \subsection{Oracles}
   400 \subsection{Oracles}
   402 
   401 
   403 \indexisarcmd{oracle}
   402 \indexisarcmd{oracle}