--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Feb 02 21:21:41 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 04 14:20:39 2012 +0100
@@ -416,45 +416,38 @@
annotations.
\begin{railoutput}
-\rail@begin{3}{\indexdef{}{syntax}{infix}\hypertarget{syntax.infix}{\hyperlink{syntax.infix}{\mbox{\isa{infix}}}}}
+\rail@begin{7}{\indexdef{}{syntax}{mixfix}\hypertarget{syntax.mixfix}{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}}
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
\rail@bar
+\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\isa{prios}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
+\rail@endbar
+\rail@nextbar{2}
+\rail@bar
\rail@term{\isa{\isakeyword{infix}}}[]
-\rail@nextbar{1}
+\rail@nextbar{3}
\rail@term{\isa{\isakeyword{infixl}}}[]
-\rail@nextbar{2}
+\rail@nextbar{4}
\rail@term{\isa{\isakeyword{infixr}}}[]
\rail@endbar
\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@end
-\rail@begin{5}{\indexdef{}{syntax}{mixfix}\hypertarget{syntax.mixfix}{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}}
-\rail@bar
-\rail@nont{\hyperlink{syntax.infix}{\mbox{\isa{infix}}}}[]
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
+\rail@nextbar{5}
+\rail@term{\isa{\isakeyword{binder}}}[]
\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
\rail@bar
-\rail@nextbar{2}
+\rail@nextbar{6}
\rail@nont{\isa{prios}}[]
\rail@endbar
-\rail@bar
-\rail@nextbar{2}
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@nextbar{3}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@term{\isa{\isakeyword{binder}}}[]
-\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
-\rail@bar
-\rail@nextbar{4}
-\rail@nont{\isa{prios}}[]
-\rail@endbar
-\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@endbar
\rail@end
\rail@begin{2}{\indexdef{}{syntax}{struct\_mixfix}\hypertarget{syntax.struct-mixfix}{\hyperlink{syntax.struct-mixfix}{\mbox{\isa{struct{\isaliteral{5F}{\isacharunderscore}}mixfix}}}}}
\rail@bar