--- a/doc-src/IsarImplementation/Thy/document/Syntax.tex Sat Apr 30 23:27:57 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex Sun May 01 00:01:59 2011 +0200
@@ -167,10 +167,21 @@
\indexdef{}{ML antiquotation}{syntax\_const}\hypertarget{ML antiquotation.syntax-const}{\hyperlink{ML antiquotation.syntax-const}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}const}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
\end{matharray}
- \begin{rail}
- ('class_syntax' | 'type_syntax' | 'const_syntax' | 'syntax_const') name
- ;
- \end{rail}
+ \begin{railoutput}
+\rail@begin{4}{\isa{}}
+\rail@bar
+\rail@term{\hyperlink{ML antiquotation.class-syntax}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{ML antiquotation.type-syntax}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
+\rail@nextbar{2}
+\rail@term{\hyperlink{ML antiquotation.const-syntax}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
+\rail@nextbar{3}
+\rail@term{\hyperlink{ML antiquotation.syntax-const}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}const}}}}[]
+\rail@endbar
+\rail@nont{\isa{name}}[]
+\rail@end
+\end{railoutput}
+
\begin{description}