Re: [isabelle] Atomisation of free variables
On 09.09.2014 18:23, Manuel Eberl wrote:
> 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.
There is forall_intr_list (in Drule), which turns free variables into
meta-quantified variables. The tactic Object_Logic.full_atomize_tac will
replace meta implication by object logic implication (and probably other
This archive was generated by a fusion of
Pipermail (Mailman edition) and