--- a/doc-src/TutorialI/Recdef/Induction.thy Fri Aug 25 12:17:09 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Induction.thy Mon Aug 28 09:32:51 2000 +0200
@@ -41,7 +41,7 @@
The rest is pure simplification:
*}
-by auto;
+by simp_all;
text{*
Try proving the above lemma by structural induction, and you find that you
@@ -58,13 +58,13 @@
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}%
-{\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%
+{\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}%
-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
+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
(in which case you may assume it holds for the tail of that list).
*}