diff -r f139d0ac2d44 -r 6c621a9d612a doc-src/IsarRef/Thy/document/ZF_Specific.tex
--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Sun May 01 18:57:45 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Mon May 02 01:05:50 2011 +0200
@@ -39,10 +39,18 @@
     \indexdef{ZF}{attribute}{TC}\hypertarget{attribute.ZF.TC}{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}} & : & \isa{attribute} \\
   \end{matharray}
 
-  \begin{rail}
-    'TC' (() | 'add' | 'del')
-    ;
-  \end{rail}
+  \begin{railoutput}
+\rail@begin{3}{\isa{}}
+\rail@term{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{add}}[]
+\rail@nextbar{2}
+\rail@term{\isa{del}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
 
   \begin{description}
   
@@ -79,41 +87,145 @@
     \indexdef{ZF}{command}{codatatype}\hypertarget{command.ZF.codatatype}{\hyperlink{command.ZF.codatatype}{\mbox{\isa{\isacommand{codatatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
   \end{matharray}
 
-  \begin{rail}
-    ('inductive' | 'coinductive') domains intros hints
-    ;
+  \begin{railoutput}
+\rail@begin{2}{\isa{}}
+\rail@bar
+\rail@term{\hyperlink{command.ZF.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{command.ZF.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}}[]
+\rail@endbar
+\rail@nont{\isa{domains}}[]
+\rail@nont{\isa{intros}}[]
+\rail@nont{\isa{hints}}[]
+\rail@end
+\rail@begin{2}{\isa{domains}}
+\rail@term{\isa{\isakeyword{domains}}}[]
+\rail@plus
+\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
+\rail@nextplus{1}
+\rail@cterm{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
+\rail@endplus
+\rail@bar
+\rail@term{\isa{{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}}}[]
+\rail@nextbar{1}
+\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
+\rail@endbar
+\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
+\rail@end
+\rail@begin{3}{\isa{intros}}
+\rail@term{\isa{\isakeyword{intros}}}[]
+\rail@plus
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
+\rail@endbar
+\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
+\rail@nextplus{2}
+\rail@endplus
+\rail@end
+\rail@begin{2}{\isa{hints}}
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\isa{condefs}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}[]
+\rail@endbar
+\rail@end
+\rail@begin{1}{\indexdef{ZF}{syntax}{monos}\hypertarget{syntax.ZF.monos}{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}}
+\rail@term{\isa{\isakeyword{monos}}}[]
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@end
+\rail@begin{1}{\isa{condefs}}
+\rail@term{\isa{\isakeyword{con{\isaliteral{5F}{\isacharunderscore}}defs}}}[]
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@end
+\rail@begin{1}{\indexdef{ZF}{syntax}{typeintros}\hypertarget{syntax.ZF.typeintros}{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}}
+\rail@term{\isa{\isakeyword{type{\isaliteral{5F}{\isacharunderscore}}intros}}}[]
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@end
+\rail@begin{1}{\indexdef{ZF}{syntax}{typeelims}\hypertarget{syntax.ZF.typeelims}{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}}
+\rail@term{\isa{\isakeyword{type{\isaliteral{5F}{\isacharunderscore}}elims}}}[]
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@end
+\end{railoutput}
 
-    domains: 'domains' (term + '+') ('<=' | subseteq) term
-    ;
-    intros: 'intros' (thmdecl? prop +)
-    ;
-    hints: monos? condefs? typeintros? typeelims?
-    ;
-    monos: ('monos' thmrefs)?
-    ;
-    condefs: ('con_defs' thmrefs)?
-    ;
-    typeintros: ('type_intros' thmrefs)?
-    ;
-    typeelims: ('type_elims' thmrefs)?
-    ;
-  \end{rail}
 
   In the following syntax specification \isa{{\isaliteral{22}{\isachardoublequote}}monos{\isaliteral{22}{\isachardoublequote}}}, \isa{typeintros}, and \isa{typeelims} are the same as above.
 
-  \begin{rail}
-    ('datatype' | 'codatatype') domain? (dtspec + 'and') hints
-    ;
+  \begin{railoutput}
+\rail@begin{2}{\isa{}}
+\rail@bar
+\rail@term{\hyperlink{command.ZF.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{command.ZF.codatatype}{\mbox{\isa{\isacommand{codatatype}}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\isa{domain}}[]
+\rail@endbar
+\rail@plus
+\rail@nont{\isa{dtspec}}[]
+\rail@nextplus{1}
+\rail@cterm{\isa{\isakeyword{and}}}[]
+\rail@endplus
+\rail@nont{\isa{hints}}[]
+\rail@end
+\rail@begin{2}{\isa{domain}}
+\rail@bar
+\rail@term{\isa{{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}}}[]
+\rail@nextbar{1}
+\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
+\rail@endbar
+\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
+\rail@end
+\rail@begin{2}{\isa{dtspec}}
+\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
+\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
+\rail@plus
+\rail@nont{\isa{con}}[]
+\rail@nextplus{1}
+\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
+\rail@endplus
+\rail@end
+\rail@begin{3}{\isa{con}}
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
+\rail@plus
+\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
+\rail@term{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
+\rail@nextplus{2}
+\rail@endplus
+\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
+\rail@endbar
+\rail@end
+\rail@begin{2}{\isa{hints}}
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
 
-    domain: ('<=' | subseteq) term
-    ;
-    dtspec: term '=' (con + '|')
-    ;
-    con: name ('(' (term ',' +) ')')?  
-    ;
-    hints: monos? typeintros? typeelims?
-    ;
-  \end{rail}
 
   See \cite{isabelle-ZF} for further information on inductive
   definitions in ZF, but note that this covers the old-style theory
@@ -130,10 +242,19 @@
     \indexdef{ZF}{command}{primrec}\hypertarget{command.ZF.primrec}{\hyperlink{command.ZF.primrec}{\mbox{\isa{\isacommand{primrec}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
   \end{matharray}
 
-  \begin{rail}
-    'primrec' (thmdecl? prop +)
-    ;
-  \end{rail}%
+  \begin{railoutput}
+\rail@begin{3}{\isa{}}
+\rail@term{\hyperlink{command.ZF.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
+\rail@plus
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
+\rail@endbar
+\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
+\rail@nextplus{2}
+\rail@endplus
+\rail@end
+\end{railoutput}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -152,14 +273,42 @@
     \indexdef{ZF}{command}{inductive\_cases}\hypertarget{command.ZF.inductive-cases}{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
   \end{matharray}
 
-  \begin{rail}
-    ('case_tac' | 'induct_tac') goalspec? name
-    ;
-    indcases (prop +)
-    ;
-    inductivecases (thmdecl? (prop +) + 'and')
-    ;
-  \end{rail}%
+  \begin{railoutput}
+\rail@begin{2}{\isa{}}
+\rail@bar
+\rail@term{\hyperlink{method.ZF.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{method.ZF.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
+\rail@endbar
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@end
+\rail@begin{2}{\isa{}}
+\rail@term{\hyperlink{method.ZF.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[]
+\rail@plus
+\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\rail@begin{3}{\isa{}}
+\rail@term{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]
+\rail@plus
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
+\rail@endbar
+\rail@plus
+\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@nextplus{2}
+\rail@cterm{\isa{\isakeyword{and}}}[]
+\rail@endplus
+\rail@end
+\end{railoutput}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %