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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and