--- a/doc-src/IsarRef/Thy/Spec.thy Sat Jun 14 15:58:36 2008 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Sat Jun 14 17:26:07 2008 +0200
@@ -1262,16 +1262,12 @@
@{command_def "print_translation"} & : & \isartrans{theory}{theory} \\
@{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\
@{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\
- @{command_def "token_translation"} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}
( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
;
-
- 'token\_translation' text
- ;
\end{rail}
Syntax translation functions written in ML admit almost arbitrary
@@ -1287,8 +1283,6 @@
val typed_print_translation :
(string * (bool -> typ -> term list -> term)) list
val print_ast_translation : (string * (ast list -> ast)) list
-val token_translation :
- (string * string * (string -> string * real)) list
\end{ttbox}
If the @{text "(advanced)"} option is given, the corresponding