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

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.