--- 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}