Re: [isabelle] Structural induction with an assumption in Isar

Thank you!  In retrospect, this makes perfect sense.

On Tue, Dec 18, 2012 at 4:23 AM, Julian Brunner <julianbrunner at>wrote:

> Hello,
> You'll want to change your proof to something like
> proof -
>   assume Asm: "Assumption S"
>   from Asm have "P S"
>   proof (induct S)
>   case (Foo arg) from Foo show ?case by simp
> That way, your assumption is included in the induction and will
> reappear as part of Foo.
> Cheers,
>  Julian

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