[isabelle] Modifying theorems



Hi

Im trying to use a simplified version of a theorem.  Using

thm lemmaName[simplified]

I get that the premisses of the simplified theorem are of the form

[|  A /\ B ; C /\ D ; E /\ F |] ==>

and the current goal has premisses of the form

[| A ; B ; C ; D ; E ; F |] ==>

so at the minute it fails. Is there any way that I can get the lemma in the appropriate form? I've tried using

lemmaName[simplified, THEN (elim conjE)]

but I get a "Bad arguments" warning. The same happens with "auto", "blast" and "force" if added in place of (elim conjE).

Cheers

Peter





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