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 MHonArc.