--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Aug 29 15:43:29 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Aug 29 16:05:13 2000 +0200
@@ -27,13 +27,13 @@
Induction variable occurs also among premises!
\end{quote}
and leads to the base case
-\begin{isabellepar}%
+\begin{isabelle}
\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
-\end{isabellepar}%
+\end{isabelle}
which, after simplification, becomes
-\begin{isabellepar}%
+\begin{isabelle}
\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
-\end{isabellepar}%
+\end{isabelle}
We cannot prove this equality because we do not know what \isa{hd} and
\isa{last} return when applied to \isa{[]}.
@@ -51,9 +51,9 @@
\begin{isamarkuptext}%
\noindent
This time, induction leaves us with the following base case
-\begin{isabellepar}%
+\begin{isabelle}
\ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
-\end{isabellepar}%
+\end{isabelle}
which is trivial, and \isa{auto} finishes the whole proof.
If \isa{hd\_rev} is meant to be a simplification rule, you are done. But if you
@@ -151,18 +151,18 @@
\begin{isamarkuptxt}%
\noindent
which leaves us with the following proof state:
-\begin{isabellepar}%
+\begin{isabelle}
\ 1.\ {\isasymAnd}\mbox{n}.\ {\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i})\isanewline
\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
-\end{isabellepar}%
+\end{isabelle}
After stripping the \isa{\isasymforall i}, the proof continues with a case
distinction on \isa{i}. The case \isa{i = 0} is trivial and we focus on the
other case:
-\begin{isabellepar}%
+\begin{isabelle}
\ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline
\ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i});\ \mbox{i}\ =\ Suc\ \mbox{nat}{\isasymrbrakk}\isanewline
\ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
-\end{isabellepar}%%
+\end{isabelle}%
\end{isamarkuptxt}%
\isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
\begin{isamarkuptext}%