[isabelle-dev] Difference between " induct " and " induct_tac "

[charmi panchal]

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

it shows error when induct_tac is used.

Thanks in advance,
Charmi Panchal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120327/bdad0445/attachment.html>