doc-src/IsarRef/Thy/document/Inner_Syntax.tex
changeset 46294 f9a1cd2599dd
parent 46293 f248b5f2783a
child 46483 10a9c31a22b4
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Tue Feb 07 18:51:22 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Tue Feb 07 18:56:40 2012 +0100
@@ -1426,9 +1426,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:
@@ -1441,7 +1438,11 @@
   (string * (Proof.context -> typ -> term list -> term)) list
 val print_ast_translation:
   (string * (Proof.context -> ast list -> ast)) list
-\end{ttbox}%
+\end{ttbox}
+
+  \medskip See also the chapter on ``Syntax Transformations'' in old
+  \cite{isabelle-ref} for further details on translations on parse
+  trees.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %