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
