Re: [isabelle] Atomisation of free variables



On 09.09.2014 18:23, Manuel Eberl wrote:
> 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.
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
stuff, too).

  -- Lars




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