--- a/doc-src/TutorialI/Recdef/document/Induction.tex Tue Aug 29 15:43:29 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Aug 29 16:05:13 2000 +0200
@@ -28,13 +28,13 @@
\noindent
The resulting proof state has three subgoals corresponding to the three
clauses for \isa{sep}:
-\begin{isabellepar}%
+\begin{isabelle}
~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
~3.~{\isasymAnd}a~x~y~zs.\isanewline
~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline
~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))%
-\end{isabellepar}%
+\end{isabelle}
The rest is pure simplification:%
\end{isamarkuptxt}%
\isacommand{by}\ simp{\isacharunderscore}all%
@@ -52,12 +52,12 @@
name of a function that takes an $n$-tuple. Usually the subgoal will
contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
induction rules do not mention $f$ at all. For example \isa{sep.induct}
-\begin{isabellepar}%
+\begin{isabelle}
{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
~~{\isasymAnd}a~x.~P~a~[x];\isanewline
~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
{\isasymLongrightarrow}~P~u~v%
-\end{isabellepar}%
+\end{isabelle}
merely says that in order to prove a property \isa{P} of \isa{u} and
\isa{v} you need to prove it for the three cases where \isa{v} is the
empty list, the singleton list, and the list with at least two elements