[isabelle] Atomisation of free variables


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?


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