*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Why is conjE so complicated? [was: Re: intro rule for &&&]*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 20 Dec 2012 22:16:06 +0100*In-reply-to*: <20121220205549.GA5275@hbl-lap-dell>*References*: <471B2DE1-DDC9-4526-8248-AFA898FB5B29@cam.ac.uk> <20121220205549.GA5275@hbl-lap-dell>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:17.0) Gecko/17.0 Thunderbird/17.0

Am 20/12/2012 21:55, schrieb Holger Blasum: > lemma conjD1: "!!A B. A & B ==> A" by simp > lemma conjD2: "!!A B. A & B ==> B" by simp ... > Is there any deeper reason "conjE" appears overly complicated Because you used it with rule, not erule. It makes perfect sense in apply scripts. > and/or "conjD1" and "conjD2" are not aboard? They are, and Proof General actually tells you so when you state conjD1: Auto solve_direct: The current goal can be solved directly with HOL.conjE: [|?P & ?Q; [|?P; ?Q|] ==> ?R|] ==> ?R HOL.conjunct1: ?P & ?Q ==> ?P Regards Tobias

**References**:**[isabelle] intro rule for &&&***From:*John Wickerson

**[isabelle] Why is conjE so complicated? [was: Re: intro rule for &&&]***From:*Holger Blasum

- Previous by Date: [isabelle] Why is conjE so complicated? [was: Re: intro rule for &&&]
- Next by Date: Re: [isabelle] Feature request: definition on crtl+hover
- Previous by Thread: [isabelle] Why is conjE so complicated? [was: Re: intro rule for &&&]
- Next by Thread: Re: [isabelle] Why is conjE so complicated? [was: Re: intro rule for &&&]
- Cl-isabelle-users December 2012 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