doc-src/TutorialI/Misc/document/cases.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/document/cases.tex	Wed Apr 19 12:59:38 2000 +0200
@@ -0,0 +1,12 @@
+\begin{isabelle}%
+\isanewline
+\isacommand{lemma}~{"}(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs{"}\isanewline
+\isacommand{apply}(case\_tac~xs)%
+\begin{isamarkuptxt}%
+\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}%%
+\end{isamarkuptxt}%
+\isacommand{apply}(auto)\isacommand{.}\isanewline
+\end{isabelle}%