[isabelle] Using an assumption as a rule



Hi all,

Say my current goal looks like:

A v ==>
(!! x. B x ==> C x) ==>
C v

Here, I have an assumption that I could easily use as an introduction rule
for my conclusion, resulting in the new goal

A v ==>
B v ==>
C v

If I were in Isar mode, the rule-shaped assumption would have a name that I
could apply using the rule tactic. Is there an easy way to do this in apply
mode? At the moment I'm repeatedly using meta_allE (my case has a few more
bound variables), but this seems dirty.

Regards,
--Ed



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