--- 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
--- 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%
%