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}