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 gmail.com>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.