*To*: noam neer <noamneer at gmail.com>*Subject*: Re: [isabelle] some problems with the /\ quantifier*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Fri, 18 Sep 2015 12:04:22 +0200*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAGOKs09Y7CF-xBX7xiOAQ-FBDFhqgXP9zxx2b7yTmtr7sVd5CQ@mail.gmail.com>*References*: <CAGOKs09PRLE1E97Sw9ri493tdjA8G3vRMAMYyWm+TBf0nfxVuA@mail.gmail.com> <55F50825.9020104@in.tum.de> <CAGOKs0_YyEvN39x-UXL6jnofDj-A2pfo35qsGxn6KSNCBKwUjA@mail.gmail.com> <55F53BB3.9030101@in.tum.de> <CAGOKs0-RRpTOfF3QAvY3f0BZu-gwKDc3k6iW2k083Yi864J0gQ@mail.gmail.com> <55FBA1BC.9060001@in.tum.de> <CAGOKs09Y7CF-xBX7xiOAQ-FBDFhqgXP9zxx2b7yTmtr7sVd5CQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.8.0

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

**Follow-Ups**:**Re: [isabelle] some problems with the /\ quantifier***From:*noam neer

**References**:**[isabelle] some problems with the /\ quantifier***From:*noam neer

**Re: [isabelle] some problems with the /\ quantifier***From:*Lars Hupel

**Re: [isabelle] some problems with the /\ quantifier***From:*noam neer

**Re: [isabelle] some problems with the /\ quantifier***From:*Lars Hupel

**Re: [isabelle] some problems with the /\ quantifier***From:*noam neer

**Re: [isabelle] some problems with the /\ quantifier***From:*Lars Noschinski

**Re: [isabelle] some problems with the /\ quantifier***From:*noam neer

- Previous by Date: Re: [isabelle] some problems with the /\ quantifier
- Next by Date: Re: [isabelle] Isabelle Foundation & Certification
- Previous by Thread: Re: [isabelle] some problems with the /\ quantifier
- Next by Thread: Re: [isabelle] some problems with the /\ quantifier
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list