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



my mistake,
it's working fine.


On Fri, Sep 18, 2015 at 1:04 PM, Lars Noschinski <noschinl at in.tum.de> wrote:

> On 18.09.2015 12:00, noam neer wrote:
> > 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
>
> That is normal: Free variables fixed in a proof are brown-ish.
>
> > simplifier doesn't work properly.
>
> What do you mean by that?
>
> > so, what should I do if I want to use the induction variable? what is
> > the parallel of 'obtain'?
>
> Just use it. "case (Suc n)" fixes an n for your use.
>
>   -- Lars
>



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