Re: [isabelle] some problems with the /\ quantifier
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