Re: [isabelle] Modifying theorems



The format is "... THEN <thm>" where ... should yield "... ==> P" and <thm> should be of the form "P ==> ..." (modulo unification). The two theorems are chained together.

Tobias

Peter Chapman schrieb:
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.