doc-src/IsarRef/Thy/Inner_Syntax.thy
changeset 46294 f9a1cd2599dd
parent 46293 f248b5f2783a
child 46483 10a9c31a22b4
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Tue Feb 07 18:51:22 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Tue Feb 07 18:56:40 2012 +0100
@@ -1179,9 +1179,6 @@
   translations functions may refer to specific theory declarations or
   auxiliary proof data.
 
-  See also \cite{isabelle-ref} for more information on the general
-  concept of syntax transformations in Isabelle.
-
 %FIXME proper antiquotations
 \begin{ttbox}
 val parse_ast_translation:
@@ -1195,6 +1192,10 @@
 val print_ast_translation:
   (string * (Proof.context -> ast list -> ast)) list
 \end{ttbox}
+
+  \medskip See also the chapter on ``Syntax Transformations'' in old
+  \cite{isabelle-ref} for further details on translations on parse
+  trees.
 *}
 
 end