I have redirected your request to isabelle-us...@cl.cam.ac.uk. That is the
appropriate mailing list for users' questions.
The developers' mailing list is for use by the Isabelle developers.
Larry Paulson
On 27 Mar 2012, at 09:14, charmi panchal wrote:
> Hello,
> I am a beginner of Isabelle an
Hello,
I am a beginner of Isabelle and practicing it in JEdit. I wish to
understand the difference between "induct" and "induct_tac"
e.g.
lemma zip1_zip2: "(zip1 xs ys) = (zip2 xs ys)"
apply (induct xs arbitrary: ys)
apply (case_tac ys)
apply auto
apply (case_tac ys)
apply auto
done
