doc-src/IsarRef/Thy/document/Misc.tex
changeset 42662 2080fe35abea
parent 42651 e3fdb7c96be5
child 46279 ddf7f79abdac
--- 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}