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



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.