Re: [isabelle] some problems with the /\ quantifier



On 18.09.2015 07:16, noam neer wrote:
> does this problem happen whenever the /\ quantifier is involved,
> or just when automatic names are generated?

Proof methods (and attributes like of, where) can usually only address
free variables -- the reason being that bound variables have no meaning
outside the subterm they were bound in.

They are a few older methods (the "_tac" family), which have special
code to match names with bound variables.

  -- Lars




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