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



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
_______________________________________________
isabelle-dev mailing list
isabelle-dev at in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.