\begin{isabelle}%
\isanewline
\isacommand{lemma}\ {"}(case\ xs\ of\ []\ {\isasymRightarrow}\ []\ |\ y\#ys\ {\isasymRightarrow}\ xs)\ =\ xs{"}\isanewline
\isacommand{apply}(case\_tac\ xs)%
\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}(auto)\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: