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}