# HG changeset patch
# User wenzelm
# Date 1304449644 -7200
# Node ID 2080fe35abea4e392d226e3c6606bfd0d1167451
# Parent  824d3f1d8de6f5f70e59cbbbb872345756575ff3
updated generated files;

diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarImplementation/Thy/document/Logic.tex
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Tue May 03 21:07:24 2011 +0200
@@ -217,15 +217,15 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.class}{\mbox{\isa{class}}}}[]
 \rail@nont{\isa{nameref}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.sort}{\mbox{\isa{sort}}}}[]
 \rail@nont{\isa{sort}}[]
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@term{\hyperlink{ML antiquotation.type-name}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}name}}}}[]
 \rail@nextbar{1}
@@ -235,7 +235,7 @@
 \rail@endbar
 \rail@nont{\isa{nameref}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.typ}{\mbox{\isa{typ}}}}[]
 \rail@nont{\isa{type}}[]
 \rail@end
@@ -481,7 +481,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{ML antiquotation.const-name}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}name}}}}[]
 \rail@nextbar{1}
@@ -489,7 +489,7 @@
 \rail@endbar
 \rail@nont{\isa{nameref}}[]
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{ML antiquotation.const}{\mbox{\isa{const}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -502,11 +502,11 @@
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.term}{\mbox{\isa{term}}}}[]
 \rail@nont{\isa{term}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.prop}{\mbox{\isa{prop}}}}[]
 \rail@nont{\isa{prop}}[]
 \rail@end
@@ -813,27 +813,27 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.ctyp}{\mbox{\isa{ctyp}}}}[]
 \rail@nont{\isa{typ}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.cterm}{\mbox{\isa{cterm}}}}[]
 \rail@nont{\isa{term}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.cprop}{\mbox{\isa{cprop}}}}[]
 \rail@nont{\isa{prop}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.thm}{\mbox{\isa{thm}}}}[]
 \rail@nont{\isa{thmref}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.thms}{\mbox{\isa{thms}}}}[]
 \rail@nont{\isa{thmrefs}}[]
 \rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
 \rail@term{\hyperlink{ML antiquotation.lemma}{\mbox{\isa{lemma}}}}[]
 \rail@bar
 \rail@nextbar{1}
diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Tue May 03 21:07:24 2011 +0200
@@ -849,7 +849,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{ML antiquotation.let}{\mbox{\isa{let}}}}[]
 \rail@plus
 \rail@plus
@@ -863,7 +863,7 @@
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{ML antiquotation.note}{\mbox{\isa{note}}}}[]
 \rail@plus
 \rail@bar
diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Tue May 03 21:07:24 2011 +0200
@@ -265,7 +265,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1721,7 +1721,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}}[]
 \rail@nont{\isa{name}}[]
 \rail@end
diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarImplementation/Thy/document/Syntax.tex
--- a/doc-src/IsarImplementation/Thy/document/Syntax.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex	Tue May 03 21:07:24 2011 +0200
@@ -168,7 +168,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
 \rail@bar
 \rail@term{\hyperlink{ML antiquotation.class-syntax}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
 \rail@nextbar{1}
diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue May 03 21:07:24 2011 +0200
@@ -103,7 +103,7 @@
   syntax.
 
   \begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
 \rail@bar
 \rail@term{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}}[]
 \rail@nextbar{1}
@@ -121,7 +121,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
 \rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
 \rail@bar
 \rail@term{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}}[]
 \rail@nextbar{1}
@@ -230,7 +230,7 @@
   context.
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}}}[]
 \rail@nont{\isa{antiquotation}}[]
 \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
@@ -642,7 +642,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\isa{rail}}[]
 \rail@nont{\isa{string}}[]
 \rail@end
@@ -658,7 +658,7 @@
   The rail specification language is quoted here as Isabelle \hyperlink{syntax.string}{\mbox{\isa{string}}}; it has its own grammar given below.
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@plus
 \rail@bar
 \rail@nextbar{1}
@@ -750,7 +750,7 @@
   \item Empty \verb|()|
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@end
 \end{railoutput}
 
@@ -758,7 +758,7 @@
   \item Nonterminal \verb|A|
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@nont{\isa{A}}[]
 \rail@end
 \end{railoutput}
@@ -768,7 +768,7 @@
   \verb|@{syntax method}|
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
 \rail@end
 \end{railoutput}
@@ -777,7 +777,7 @@
   \item Terminal \verb|'xyz'|
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\isa{xyz}}[]
 \rail@end
 \end{railoutput}
@@ -786,7 +786,7 @@
   \item Terminal in keyword style \verb|@'xyz'|
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\isa{\isakeyword{xyz}}}[]
 \rail@end
 \end{railoutput}
@@ -796,7 +796,7 @@
   \verb|@@{method rule}|
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
 \rail@end
 \end{railoutput}
@@ -805,7 +805,7 @@
   \item Concatenation \verb|A B C|
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@nont{\isa{A}}[]
 \rail@nont{\isa{B}}[]
 \rail@nont{\isa{C}}[]
@@ -819,7 +819,7 @@
   second one for escaping.} \verb|A B C \\ D E F|
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@nont{\isa{A}}[]
 \rail@nont{\isa{B}}[]
 \rail@nont{\isa{C}}[]
@@ -834,7 +834,7 @@
   \item Variants \verb|A |\verb,|,\verb| B |\verb,|,\verb| C|
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@nont{\isa{A}}[]
 \rail@nextbar{1}
@@ -849,7 +849,7 @@
   \item Option \verb|A ?|
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\isa{A}}[]
@@ -861,7 +861,7 @@
   \item Repetition \verb|A *|
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@plus
 \rail@nextplus{1}
 \rail@cnont{\isa{A}}[]
@@ -873,7 +873,7 @@
   \item Repetition with separator \verb|A * sep|
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@nextbar{1}
 \rail@plus
@@ -889,7 +889,7 @@
   \item Strict repetition \verb|A +|
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@plus
 \rail@nont{\isa{A}}[]
 \rail@nextplus{1}
@@ -901,7 +901,7 @@
   \item Strict repetition with separator \verb|A + sep|
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@plus
 \rail@nont{\isa{A}}[]
 \rail@nextplus{1}
@@ -926,7 +926,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isaliteral{5F}{\isacharunderscore}}drafts}}}}}[]
 \rail@nextbar{1}
diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Tue May 03 21:07:24 2011 +0200
@@ -72,7 +72,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -128,7 +128,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@term{\hyperlink{method.fold}{\mbox{\isa{fold}}}}[]
 \rail@nextbar{1}
@@ -138,7 +138,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@term{\hyperlink{method.erule}{\mbox{\isa{erule}}}}[]
 \rail@nextbar{1}
@@ -206,16 +206,16 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}}[]
 \rail@nextbar{1}
@@ -229,7 +229,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}}[]
 \rail@nextbar{1}
@@ -237,7 +237,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -297,7 +297,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{method.subst}{\mbox{\isa{subst}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -316,7 +316,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.split}{\mbox{\isa{split}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -426,7 +426,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
 \rail@bar
 \rail@term{\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \rail@nextbar{1}
@@ -452,7 +452,7 @@
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -463,7 +463,7 @@
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -474,7 +474,7 @@
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -485,7 +485,7 @@
 \rail@nont{\hyperlink{syntax.int}{\mbox{\isa{int}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{method.tactic}{\mbox{\isa{tactic}}}}[]
 \rail@nextbar{1}
@@ -570,7 +570,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{method.simp}{\mbox{\isa{simp}}}}[]
 \rail@nextbar{1}
@@ -693,7 +693,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@term{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}}[]
 \rail@nextbar{1}
@@ -738,7 +738,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
 \rail@term{\hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
@@ -760,7 +760,7 @@
 \rail@endplus
 \rail@endbar
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{attribute.simproc}{\mbox{\isa{simproc}}}}[]
 \rail@bar
 \rail@bar
@@ -818,7 +818,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{attribute.simplified}{\mbox{\isa{simplified}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -877,7 +877,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
 \rail@nextbar{1}
@@ -936,7 +936,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.blast}{\mbox{\isa{blast}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -947,7 +947,7 @@
 \rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
 \rail@bar
 \rail@term{\hyperlink{method.fast}{\mbox{\isa{fast}}}}[]
 \rail@nextbar{1}
@@ -1022,7 +1022,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.auto}{\mbox{\isa{auto}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1034,7 +1034,7 @@
 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
 \rail@bar
 \rail@term{\hyperlink{method.force}{\mbox{\isa{force}}}}[]
 \rail@nextbar{1}
@@ -1146,7 +1146,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[]
 \rail@nextbar{1}
@@ -1165,11 +1165,11 @@
 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}}[]
 \rail@term{\isa{del}}[]
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}}[]
 \rail@bar
 \rail@bar
@@ -1272,11 +1272,11 @@
   declarations internally.
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}}[]
 \rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1285,7 +1285,7 @@
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
 \rail@bar
 \rail@nextbar{1}
diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarRef/Thy/document/HOLCF_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Tue May 03 21:07:24 2011 +0200
@@ -55,7 +55,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOLCF.domain}{\mbox{\isa{\isacommand{domain}}}}}[]
 \rail@bar
 \rail@nextbar{1}
diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue May 03 21:07:24 2011 +0200
@@ -32,7 +32,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -123,7 +123,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -237,7 +237,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
 \rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -410,7 +410,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
 \rail@plus
 \rail@nont{\isa{dtspec}}[]
@@ -418,7 +418,7 @@
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -499,7 +499,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -552,7 +552,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -562,7 +562,7 @@
 \rail@term{\isa{\isakeyword{where}}}[]
 \rail@nont{\isa{equations}}[]
 \rail@end
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
 \rail@bar
 \rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[]
 \rail@nextbar{1}
@@ -605,7 +605,7 @@
 \rail@endplus
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -696,18 +696,18 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[]
 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[]
 \rail@plus
 \rail@nextplus{1}
 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[]
 \rail@nont{\isa{orders}}[]
 \rail@plus
@@ -781,7 +781,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
 \rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -866,7 +866,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
 \rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -886,7 +886,7 @@
 \rail@nont{\isa{hints}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@nont{\isa{recdeftc}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -968,7 +968,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[]
 \rail@nextbar{1}
@@ -1023,7 +1023,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
 \rail@bar
 \rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
 \rail@nextbar{1}
@@ -1066,7 +1066,7 @@
 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1210,7 +1210,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}}[]
 \rail@plus
 \rail@nextplus{1}
@@ -1246,7 +1246,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1281,7 +1281,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
 \rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1305,7 +1305,7 @@
 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1322,7 +1322,7 @@
 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1407,7 +1407,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1421,7 +1421,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@term{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}[]
 \rail@nextbar{1}
@@ -1440,7 +1440,7 @@
 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@term{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
 \rail@nextbar{1}
@@ -1599,7 +1599,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1611,7 +1611,7 @@
 \rail@nont{\isa{rule}}[]
 \rail@endbar
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1630,7 +1630,7 @@
 \rail@nont{\isa{rule}}[]
 \rail@endbar
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
@@ -1645,7 +1645,7 @@
 \rail@endplus
 \rail@endbar
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]
 \rail@plus
 \rail@bar
@@ -1751,7 +1751,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{11}{\isa{}}
+\rail@begin{11}{}
 \rail@term{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
 \rail@plus
 \rail@nont{\isa{constexpr}}[]
@@ -1817,7 +1817,7 @@
 \rail@term{\isa{Scala}}[]
 \rail@endbar
 \rail@end
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
 \rail@term{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1830,35 +1830,35 @@
 \rail@endbar
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}}[]
 \rail@plus
 \rail@nont{\isa{const}}[]
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
 \rail@plus
 \rail@nont{\isa{const}}[]
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@term{\isa{del}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@term{\isa{del}}[]
 \rail@endbar
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1868,7 +1868,7 @@
 \rail@endplus
 \rail@endbar
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1878,7 +1878,7 @@
 \rail@endplus
 \rail@endbar
 \rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
 \rail@term{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}}}[]
 \rail@plus
 \rail@nont{\isa{const}}[]
@@ -1901,7 +1901,7 @@
 \rail@nextplus{6}
 \rail@endplus
 \rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
 \rail@term{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
 \rail@plus
 \rail@nont{\isa{typeconstructor}}[]
@@ -1924,7 +1924,7 @@
 \rail@nextplus{6}
 \rail@endplus
 \rail@end
-\rail@begin{9}{\isa{}}
+\rail@begin{9}{}
 \rail@term{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]
 \rail@plus
 \rail@nont{\isa{class}}[]
@@ -1948,7 +1948,7 @@
 \rail@nextplus{8}
 \rail@endplus
 \rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
 \rail@term{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}}}[]
 \rail@plus
 \rail@nont{\isa{typeconstructor}}[]
@@ -1973,7 +1973,7 @@
 \rail@nextplus{6}
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}}}[]
 \rail@nont{\isa{target}}[]
 \rail@plus
@@ -1981,13 +1981,13 @@
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}}}[]
 \rail@nont{\isa{const}}[]
 \rail@nont{\isa{const}}[]
 \rail@nont{\isa{target}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}}[]
 \rail@nont{\isa{target}}[]
 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
@@ -1997,7 +1997,7 @@
 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}}}[]
 \rail@nont{\isa{target}}[]
 \rail@plus
@@ -2006,7 +2006,7 @@
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
-\rail@begin{11}{\isa{}}
+\rail@begin{11}{}
 \rail@term{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}}[]
 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
 \rail@cr{2}
@@ -2189,7 +2189,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{11}{\isa{}}
+\rail@begin{11}{}
 \rail@bar
 \rail@term{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]
 \rail@nextbar{1}
@@ -2241,7 +2241,7 @@
 \rail@endplus
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
 \rail@plus
 \rail@nont{\isa{codespec}}[]
@@ -2256,7 +2256,7 @@
 \rail@nont{\isa{attachment}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
 \rail@plus
 \rail@nont{\isa{tycodespec}}[]
@@ -2289,7 +2289,7 @@
 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
 \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -2565,7 +2565,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
 \rail@bar
 \rail@term{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}}[]
 \rail@nextbar{1}
diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Tue May 03 21:07:24 2011 +0200
@@ -45,7 +45,7 @@
   internal logical entities in a human-readable fashion.
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -53,7 +53,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -61,7 +61,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -69,7 +69,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -77,7 +77,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}[]
 \rail@nextbar{1}
@@ -92,7 +92,7 @@
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -488,7 +488,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
 \rail@bar
 \rail@term{\hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}notation}}}}}[]
 \rail@nextbar{1}
@@ -510,7 +510,7 @@
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
 \rail@bar
 \rail@term{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}}[]
 \rail@nextbar{1}
@@ -532,7 +532,7 @@
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -899,7 +899,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
@@ -907,7 +907,7 @@
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}}[]
 \rail@nextbar{1}
@@ -922,7 +922,7 @@
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
 \rail@bar
 \rail@term{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}}[]
 \rail@nextbar{1}
@@ -1017,7 +1017,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
 \rail@bar
 \rail@term{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[]
 \rail@nextbar{1}
diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarRef/Thy/document/Misc.tex
--- a/doc-src/IsarRef/Thy/document/Misc.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Misc.tex	Tue May 03 21:07:24 2011 +0200
@@ -42,7 +42,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theory}}}}}[]
 \rail@nextbar{1}
@@ -53,7 +53,7 @@
 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
 \rail@term{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -99,7 +99,7 @@
 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}}[]
 \rail@plus
 \rail@nextplus{1}
@@ -123,11 +123,11 @@
 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -259,7 +259,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}[]
 \rail@nextbar{1}
diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Tue May 03 21:07:24 2011 +0200
@@ -75,11 +75,11 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.notepad}{\mbox{\isa{\isacommand{notepad}}}}}[]
 \rail@term{\isa{\isakeyword{begin}}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}}[]
 \rail@end
 \end{railoutput}
@@ -220,7 +220,7 @@
   exporting some result \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} yields \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}t{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}.
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
@@ -228,7 +228,7 @@
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}}[]
 \rail@nextbar{1}
@@ -240,7 +240,7 @@
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}}[]
 \rail@plus
 \rail@nont{\isa{def}}[]
@@ -331,7 +331,7 @@
   input process just after type checking.  Also note that \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} does not support polymorphism.
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}}[]
 \rail@plus
 \rail@plus
@@ -403,7 +403,7 @@
   issuing a follow-up claim.
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}}[]
 \rail@plus
 \rail@bar
@@ -415,7 +415,7 @@
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
 \rail@bar
 \rail@term{\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}}[]
 \rail@nextbar{1}
@@ -538,7 +538,7 @@
   and assumptions, cf.\ \secref{sec:obtain}).
 
   \begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
 \rail@bar
 \rail@term{\hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}}[]
 \rail@nextbar{1}
@@ -562,7 +562,7 @@
 \rail@nont{\isa{longgoal}}[]
 \rail@endbar
 \rail@end
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
 \rail@bar
 \rail@term{\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}}[]
 \rail@nextbar{1}
@@ -574,7 +574,7 @@
 \rail@endbar
 \rail@nont{\isa{goal}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -849,21 +849,21 @@
   assumption in the very last step.
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\isa{method}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\isa{method}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}}[]
 \rail@nont{\isa{method}}[]
 \rail@bar
@@ -871,7 +871,7 @@
 \rail@nont{\isa{method}}[]
 \rail@endbar
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@term{\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}}[]
 \rail@nextbar{1}
@@ -954,14 +954,14 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.fact}{\mbox{\isa{fact}}}}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -993,7 +993,7 @@
 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[]
 \rail@nextbar{1}
@@ -1012,15 +1012,15 @@
 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}}[]
 \rail@term{\isa{del}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}}[]
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{attribute.of}{\mbox{\isa{of}}}}[]
 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
 \rail@bar
@@ -1030,7 +1030,7 @@
 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
 \rail@term{\hyperlink{attribute.where}{\mbox{\isa{where}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1160,7 +1160,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}}[]
 \rail@nextbar{1}
@@ -1168,14 +1168,14 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}}[]
 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
 \rail@end
@@ -1234,7 +1234,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -1309,7 +1309,7 @@
   occur in the conclusion.
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1327,7 +1327,7 @@
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
@@ -1441,7 +1441,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}}[]
 \rail@nextbar{1}
@@ -1454,7 +1454,7 @@
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{attribute.trans}{\mbox{\isa{trans}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1566,7 +1566,7 @@
   later.
 
   \begin{railoutput}
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
 \rail@term{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}}[]
 \rail@bar
 \rail@nont{\isa{caseref}}[]
@@ -1591,14 +1591,14 @@
 \rail@nont{\isa{attributes}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@plus
@@ -1606,7 +1606,7 @@
 \rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{attribute.params}{\mbox{\isa{params}}}}[]
 \rail@plus
 \rail@plus
@@ -1617,7 +1617,7 @@
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1700,7 +1700,7 @@
   ``strengthened'' inductive statements within the object-logic.
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1721,7 +1721,7 @@
 \rail@nont{\isa{rule}}[]
 \rail@endbar
 \rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
 \rail@term{\hyperlink{method.induct}{\mbox{\isa{induct}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1751,7 +1751,7 @@
 \rail@nont{\isa{rule}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}}[]
 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
 \rail@nont{\isa{taking}}[]
@@ -1987,15 +1987,15 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}}[]
 \rail@nont{\isa{spec}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}}[]
 \rail@nont{\isa{spec}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}}[]
 \rail@nont{\isa{spec}}[]
 \rail@end
diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Tue May 03 21:07:24 2011 +0200
@@ -69,7 +69,7 @@
   admissible.
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@term{\isa{\isakeyword{imports}}}[]
@@ -145,7 +145,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@term{\isa{\isakeyword{begin}}}[]
@@ -220,7 +220,7 @@
   available, and result names need not be given.
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -232,7 +232,7 @@
 \rail@nont{\isa{specs}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -249,7 +249,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -383,7 +383,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}}[]
 \rail@nextbar{1}
@@ -401,7 +401,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -568,7 +568,7 @@
   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
   \indexisarelem{defines}\indexisarelem{notes}
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@bar
@@ -581,7 +581,7 @@
 \rail@term{\isa{\isakeyword{begin}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locale}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -783,7 +783,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}}[]
 \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
 \rail@bar
@@ -791,7 +791,7 @@
 \rail@nont{\isa{equations}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}}[]
 \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
 \rail@bar
@@ -799,7 +799,7 @@
 \rail@nont{\isa{equations}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}}[]
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
 \rail@bar
@@ -813,7 +813,7 @@
 \rail@nont{\isa{equations}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -821,7 +821,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}[]
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
 \rail@end
@@ -965,7 +965,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{8}{\isa{}}
+\rail@begin{8}{}
 \rail@term{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -990,7 +990,7 @@
 \rail@term{\isa{\isakeyword{begin}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
@@ -1001,10 +1001,10 @@
 \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]
 \rail@term{\isa{\isakeyword{begin}}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
@@ -1014,7 +1014,7 @@
 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
 \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1022,7 +1022,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
 \rail@bar
@@ -1032,10 +1032,10 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
 \rail@end
 \end{railoutput}
@@ -1197,7 +1197,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
 \rail@term{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}}[]
 \rail@cr{2}
 \rail@plus
@@ -1259,11 +1259,11 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
 \rail@bar
 \rail@term{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}}[]
 \rail@nextbar{1}
@@ -1279,7 +1279,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -1383,14 +1383,14 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.classdecl}{\mbox{\isa{classdecl}}}}[]
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
@@ -1404,7 +1404,7 @@
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isaliteral{5F}{\isacharunderscore}}sort}}}}}[]
 \rail@nont{\hyperlink{syntax.sort}{\mbox{\isa{sort}}}}[]
 \rail@end
@@ -1453,7 +1453,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}}[]
 \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -1463,7 +1463,7 @@
 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}}[]
 \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
 \rail@bar
@@ -1471,7 +1471,7 @@
 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
@@ -1553,7 +1553,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
@@ -1566,7 +1566,7 @@
 \rail@nextplus{2}
 \rail@endplus
 \rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
 \rail@term{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1626,7 +1626,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[]
@@ -1634,7 +1634,7 @@
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@term{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}}[]
 \rail@nextbar{1}
@@ -1704,7 +1704,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -1743,7 +1743,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
 \rail@bar
 \rail@nont{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]
 \rail@nextbar{1}
diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarRef/Thy/document/ZF_Specific.tex
--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Tue May 03 21:07:24 2011 +0200
@@ -40,7 +40,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -88,7 +88,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{command.ZF.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
 \rail@nextbar{1}
@@ -163,7 +163,7 @@
   In the following syntax specification \isa{{\isaliteral{22}{\isachardoublequote}}monos{\isaliteral{22}{\isachardoublequote}}}, \isa{typeintros}, and \isa{typeelims} are the same as above.
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{command.ZF.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
 \rail@nextbar{1}
@@ -243,7 +243,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{command.ZF.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
 \rail@plus
 \rail@bar
@@ -274,7 +274,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{method.ZF.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \rail@nextbar{1}
@@ -286,14 +286,14 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \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@begin{3}{}
 \rail@term{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]
 \rail@plus
 \rail@bar