--- a/doc-src/TutorialI/Misc/cases.thy Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/cases.thy Tue Apr 25 08:09:10 2000 +0200
@@ -5,11 +5,13 @@
lemma "(case xs of [] \\<Rightarrow> [] | y#ys \\<Rightarrow> xs) = xs";
apply(case_tac xs);
-txt{*
+txt{*\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:
*}
apply(auto).;