--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue May 03 21:07:24 2011 +0200
@@ -32,7 +32,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -123,7 +123,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -237,7 +237,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
\rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -410,7 +410,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
\rail@plus
\rail@nont{\isa{dtspec}}[]
@@ -418,7 +418,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -499,7 +499,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -552,7 +552,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -562,7 +562,7 @@
\rail@term{\isa{\isakeyword{where}}}[]
\rail@nont{\isa{equations}}[]
\rail@end
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
\rail@bar
\rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[]
\rail@nextbar{1}
@@ -605,7 +605,7 @@
\rail@endplus
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -696,18 +696,18 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[]
\rail@plus
\rail@nextplus{1}
\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[]
\rail@nont{\isa{orders}}[]
\rail@plus
@@ -781,7 +781,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
\rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -866,7 +866,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
\rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -886,7 +886,7 @@
\rail@nont{\isa{hints}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@nont{\isa{recdeftc}}[]
\rail@bar
\rail@nextbar{1}
@@ -968,7 +968,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[]
\rail@nextbar{1}
@@ -1023,7 +1023,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
\rail@bar
\rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
\rail@nextbar{1}
@@ -1066,7 +1066,7 @@
\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
\rail@endplus
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1210,7 +1210,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}}[]
\rail@plus
\rail@nextplus{1}
@@ -1246,7 +1246,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1281,7 +1281,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1305,7 +1305,7 @@
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1322,7 +1322,7 @@
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1407,7 +1407,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1421,7 +1421,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}[]
\rail@nextbar{1}
@@ -1440,7 +1440,7 @@
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
\rail@nextbar{1}
@@ -1599,7 +1599,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1611,7 +1611,7 @@
\rail@nont{\isa{rule}}[]
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1630,7 +1630,7 @@
\rail@nont{\isa{rule}}[]
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
@@ -1645,7 +1645,7 @@
\rail@endplus
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]
\rail@plus
\rail@bar
@@ -1751,7 +1751,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{11}{\isa{}}
+\rail@begin{11}{}
\rail@term{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
\rail@plus
\rail@nont{\isa{constexpr}}[]
@@ -1817,7 +1817,7 @@
\rail@term{\isa{Scala}}[]
\rail@endbar
\rail@end
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
\rail@term{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1830,35 +1830,35 @@
\rail@endbar
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}}[]
\rail@plus
\rail@nont{\isa{const}}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
\rail@plus
\rail@nont{\isa{const}}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{del}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{del}}[]
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1868,7 +1868,7 @@
\rail@endplus
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1878,7 +1878,7 @@
\rail@endplus
\rail@endbar
\rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
\rail@term{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}}}[]
\rail@plus
\rail@nont{\isa{const}}[]
@@ -1901,7 +1901,7 @@
\rail@nextplus{6}
\rail@endplus
\rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
\rail@term{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
\rail@plus
\rail@nont{\isa{typeconstructor}}[]
@@ -1924,7 +1924,7 @@
\rail@nextplus{6}
\rail@endplus
\rail@end
-\rail@begin{9}{\isa{}}
+\rail@begin{9}{}
\rail@term{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]
\rail@plus
\rail@nont{\isa{class}}[]
@@ -1948,7 +1948,7 @@
\rail@nextplus{8}
\rail@endplus
\rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
\rail@term{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}}}[]
\rail@plus
\rail@nont{\isa{typeconstructor}}[]
@@ -1973,7 +1973,7 @@
\rail@nextplus{6}
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}}}[]
\rail@nont{\isa{target}}[]
\rail@plus
@@ -1981,13 +1981,13 @@
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}}}[]
\rail@nont{\isa{const}}[]
\rail@nont{\isa{const}}[]
\rail@nont{\isa{target}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}}[]
\rail@nont{\isa{target}}[]
\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
@@ -1997,7 +1997,7 @@
\rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}}}[]
\rail@nont{\isa{target}}[]
\rail@plus
@@ -2006,7 +2006,7 @@
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{11}{\isa{}}
+\rail@begin{11}{}
\rail@term{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}}[]
\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
\rail@cr{2}
@@ -2189,7 +2189,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{11}{\isa{}}
+\rail@begin{11}{}
\rail@bar
\rail@term{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]
\rail@nextbar{1}
@@ -2241,7 +2241,7 @@
\rail@endplus
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
\rail@plus
\rail@nont{\isa{codespec}}[]
@@ -2256,7 +2256,7 @@
\rail@nont{\isa{attachment}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
\rail@plus
\rail@nont{\isa{tycodespec}}[]
@@ -2289,7 +2289,7 @@
\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -2565,7 +2565,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@bar
\rail@term{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}}[]
\rail@nextbar{1}