--- a/doc-src/TutorialI/Misc/document/cases.tex Tue Aug 29 15:13:10 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-\begin{isabelle}%
-%
-\isamarkupsubsection{Structural induction and case distinction}
-%
-\begin{isamarkuptext}%
-\indexbold{structural induction}
-\indexbold{induction!structural}
-\indexbold{case distinction}
-Almost all the basic laws about a datatype are applied automatically during
-simplification. Only induction is invoked by hand via \isaindex{induct_tac},
-which works for any datatype. In some cases, induction is overkill and a case
-distinction over all constructors of the datatype suffices. This is performed
-by \isaindexbold{case_tac}. A trivial example:%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
-\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}%
-\begin{isamarkuptxt}%
-\noindent
-results in the proof state
-\begin{isabellepar}%
-~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
-~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
-\end{isabellepar}%
-which is solved automatically:%
-\end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
-\begin{isamarkuptext}%
-Note that we do not need to give a lemma a name if we do not intend to refer
-to it explicitly in the future.%
-\end{isamarkuptext}%
-\end{isabelle}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: