I have redirected your request to [email protected]. 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 > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
