*To*: Alexander Katovsky <apk32 at cam.ac.uk>*Subject*: Re: [isabelle] apply proof method to all subgoals*From*: Makarius <makarius at sketis.net>*Date*: Sun, 17 Apr 2011 22:12:45 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk, Mathieu Giorgino <mathieu.giorgino at irit.fr>*In-reply-to*: <4DAAC9E5.2020904@cam.ac.uk>*References*: <4DA19929.4080101@cam.ac.uk> <D5907011-347A-4FA7-8B8A-F597873FEE3A@cam.ac.uk> <4DA1BC66.9090007@cam.ac.uk> <201104101643.38161.mathieu.giorgino@irit.fr> <4DAAC9E5.2020904@cam.ac.uk>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Sun, 17 Apr 2011, Alexander Katovsky wrote:

How about lemma "\<forall> z . ((A (n :: nat) z) \<and> (B n z)) \<longrightarrow> C z" proof(induct n, intro allI conjI impI)It seems `intro` is not attacking the second induction goal. `safe` workshere, but in other cases (with particular forms for A B and C) it does morethan I want it to.

notepad begin fix z :: 'a and n :: nat have "A n z ==> B n z ==> C z" proof (induct n) ... No "intro" boilerplate is needed here. Makarius

**Follow-Ups**:**Re: [isabelle] apply proof method to all subgoals***From:*Makarius

**References**:**[isabelle] apply proof method to all subgoals***From:*Alex Katovsky

**Re: [isabelle] apply proof method to all subgoals***From:*Lawrence Paulson

**Re: [isabelle] apply proof method to all subgoals***From:*Alex Katovsky

**Re: [isabelle] apply proof method to all subgoals***From:*Mathieu Giorgino

**Re: [isabelle] apply proof method to all subgoals***From:*Alexander Katovsky

- Previous by Date: Re: [isabelle] apply proof method to all subgoals
- Next by Date: Re: [isabelle] apply proof method to all subgoals
- Previous by Thread: Re: [isabelle] apply proof method to all subgoals
- Next by Thread: Re: [isabelle] apply proof method to all subgoals
- Cl-isabelle-users April 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list