[isabelle] Atomisation of free variables



Hallo,

I need a tactic that turns something like P a b c ==> Q a b c into ALL a b c. P a b c --> Q a b c.

How do I do this?

Manuel


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