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

[Lawrence Paulson]

I have redirected your request to isabelle-users at 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 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