--- a/doc-src/IsarRef/Thy/document/Proof.tex Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Tue May 03 21:07:24 2011 +0200
@@ -75,11 +75,11 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.notepad}{\mbox{\isa{\isacommand{notepad}}}}}[]
\rail@term{\isa{\isakeyword{begin}}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}}[]
\rail@end
\end{railoutput}
@@ -220,7 +220,7 @@
exporting some result \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} yields \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}t{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}.
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
@@ -228,7 +228,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}}[]
\rail@nextbar{1}
@@ -240,7 +240,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}}[]
\rail@plus
\rail@nont{\isa{def}}[]
@@ -331,7 +331,7 @@
input process just after type checking. Also note that \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} does not support polymorphism.
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}}[]
\rail@plus
\rail@plus
@@ -403,7 +403,7 @@
issuing a follow-up claim.
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}}[]
\rail@plus
\rail@bar
@@ -415,7 +415,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
\rail@bar
\rail@term{\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}}[]
\rail@nextbar{1}
@@ -538,7 +538,7 @@
and assumptions, cf.\ \secref{sec:obtain}).
\begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@bar
\rail@term{\hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}}[]
\rail@nextbar{1}
@@ -562,7 +562,7 @@
\rail@nont{\isa{longgoal}}[]
\rail@endbar
\rail@end
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
\rail@bar
\rail@term{\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}}[]
\rail@nextbar{1}
@@ -574,7 +574,7 @@
\rail@endbar
\rail@nont{\isa{goal}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -849,21 +849,21 @@
assumption in the very last step.
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{method}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{method}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}}[]
\rail@nont{\isa{method}}[]
\rail@bar
@@ -871,7 +871,7 @@
\rail@nont{\isa{method}}[]
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}}[]
\rail@nextbar{1}
@@ -954,14 +954,14 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.fact}{\mbox{\isa{fact}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -993,7 +993,7 @@
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[]
\rail@nextbar{1}
@@ -1012,15 +1012,15 @@
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}}[]
\rail@term{\isa{del}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.of}{\mbox{\isa{of}}}}[]
\rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
\rail@bar
@@ -1030,7 +1030,7 @@
\rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
\rail@endbar
\rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@term{\hyperlink{attribute.where}{\mbox{\isa{where}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1160,7 +1160,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}}[]
\rail@nextbar{1}
@@ -1168,14 +1168,14 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}}[]
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@end
@@ -1234,7 +1234,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -1309,7 +1309,7 @@
occur in the conclusion.
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1327,7 +1327,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
@@ -1441,7 +1441,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}}[]
\rail@nextbar{1}
@@ -1454,7 +1454,7 @@
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{attribute.trans}{\mbox{\isa{trans}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1566,7 +1566,7 @@
later.
\begin{railoutput}
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
\rail@term{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}}[]
\rail@bar
\rail@nont{\isa{caseref}}[]
@@ -1591,14 +1591,14 @@
\rail@nont{\isa{attributes}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@plus
@@ -1606,7 +1606,7 @@
\rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@endplus
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{attribute.params}{\mbox{\isa{params}}}}[]
\rail@plus
\rail@plus
@@ -1617,7 +1617,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1700,7 +1700,7 @@
``strengthened'' inductive statements within the object-logic.
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1721,7 +1721,7 @@
\rail@nont{\isa{rule}}[]
\rail@endbar
\rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@term{\hyperlink{method.induct}{\mbox{\isa{induct}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1751,7 +1751,7 @@
\rail@nont{\isa{rule}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}}[]
\rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
\rail@nont{\isa{taking}}[]
@@ -1987,15 +1987,15 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}}[]
\rail@nont{\isa{spec}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}}[]
\rail@nont{\isa{spec}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}}[]
\rail@nont{\isa{spec}}[]
\rail@end