*To*: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] intro rule for &&&*From*: John Wickerson <jpw48 at cam.ac.uk>*Date*: Thu, 20 Dec 2012 12:02:12 +0100

Dear Isabelle, When I type... > lemma assumes "A ∧ B" shows "A" "B" > using assms > apply rule ...I obtain the following proof state... > goal (2 subgoals): > 1. A ⟹ B ⟹ A > 2. B ... which is insoluble. I think the "apply rule" step is using the conjE rule. Which rule should I apply in order to obtain the preferred proof state below? I briefly tried conjunctionI but that doesn't seem quite to fit. > goal (2 subgoals): > 1. A ⟹ B ⟹ A > 2. A ⟹ B ⟹ B By the way, I know I can solve this lemma via auto; my question is pedagogical rather than practical. cheers, john

**Follow-Ups**:**Re: [isabelle] intro rule for &&&***From:*Joachim Breitner

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

**Re: [isabelle] intro rule for &&&***From:*Makarius

- Previous by Date: Re: [isabelle] LaTeX Theorem Environments for Definitions and Proofs
- Next by Date: [isabelle] Fwd: Isabelle2012 - What distribution?
- Previous by Thread: Re: [isabelle] LaTeX Theorem Environments for Definitions and Proofs
- Next by Thread: Re: [isabelle] 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