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