Re: [isabelle] some problems with the /\ quantifier
OK, I just tried the Isar form of induction that starts with
proof (induction n)
and when I reached
case (Suc n)
it seems there are still problems. the 'n' has different color and the
simplifier doesn't work properly.
so, what should I do if I want to use the induction variable? what is the
parallel of 'obtain'?
On Fri, Sep 18, 2015 at 8:31 AM, Lars Noschinski <noschinl at in.tum.de> wrote:
> 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