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:
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and