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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and