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