Re: [isabelle] Problem with Isar/Isabelle Induct method
On Fri, 29 Jun 2007, Peter Chapman wrote:
> I have written an inductive proof in Isabelle, and was trying to rewrite
> it in Isar/Isabelle style to be human readable. Following the document
> "Structured Induction Proofs in Isabelle/Isar", I wrote
> lemma isar_many_step_from_list:
> proof (induct X fixing: "Gam")
> but got the error
> *** Error in method "HOL.induct":
> *** method "HOL.induct": bad arguments
> *** : "Gam"
> *** At command "proof".
Unfortunately, the present syntax of the "induct" method (of Isabelle2007
development snapshots) is no longer that of the mentioned paper. The
"fixing" part is now introcuded by "arbitrary". See also the NEWS and the
isar-ref manual on the "induct" method.
> but I cannot refer each case, so in the first case for X=[ ], I cannot
> write case "[ ]"
Note that the 'print_cases' command (or corresponding Proof General
menu/key) will show the cases available in the present proof context.
(Some of these may stem from earlier method invocations, and be no longer
This archive was generated by a fusion of
Pipermail (Mailman edition) and