*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Isabelle problem*From*: "Beta Ziliani" <beta.ziliani at gmail.com>*Date*: Fri, 6 Jun 2008 12:02:41 -0300*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <a7f3f2e30806060734j3e01c70cw7c60200ddcb09125@mail.gmail.com>*References*: <a7f3f2e30806040642j3583886dyed578ae5152bebb8@mail.gmail.com> <Pine.LNX.4.64.0806051402230.8309@macbroy20.informatik.tu-muenchen.de> <a7f3f2e30806060734j3e01c70cw7c60200ddcb09125@mail.gmail.com>

I think I know what the problem is: I have to specify Isabelle which buffer to use. That was not on the tutorial... Now I have another problem: When I use the buffer with the ToyList, it complains saying that *** Outer syntax error: keyword "=" expected, *** but identifier a was found And the text theory ToyList imports PreList begin is marked. But now mi context IS theory ToyList. And still nothing works: value "rev (True # False # [])" throws *** Inner lexical error at: "# False # [])" *** At command "value". like it didn't parse the theory. What I'm doing wrong???? :'( Thanks again, Beta On Fri, Jun 6, 2008 at 11:34 AM, Beta Ziliani <beta.ziliani at gmail.com> wrote: > Thank you Makarious and Florian, but I'm still getting the same message > with the theory opened. What else could it be? > Just to give more information, whenever I try > > normal form "rev (a # b # c # [])" > > It says that "Command is not state preserving, I won't execute it!" > > > Thanks, > Beta > > > On Thu, Jun 5, 2008 at 9:05 AM, Makarius <makarius at sketis.net> wrote: > >> On Wed, 4 Jun 2008, Beta Ziliani wrote: >> >> > I've this problem using X-Isabelle. I've just downloaded Isabelle, with >> > Emacs 21.4.20 in a Kubuntu 7.10. Looking at the tutorial I put this >> simple >> > excercise >> > >> > theory ToyList >> > imports PreList >> > begin >> > ... >> > end >> > >> > But whenever I want to do something useful , like use the command (by >> > pressing the Command button in the Proof General Toolbar) >> > >> > value "rev (True # False # [])" >> > >> > Isabelle respond with a >> > *** Illegal application of command "value" at top level >> > *** At command "value". >> > >> > I'm making things wrong, or my installation is wrong? >> >> If you have come that far then the installation is fine. You are merely >> experiencing a logical problem, trying to refer to formal entities without >> a theory context: the 'value' command needs to be issued while the theory >> is still open, before the final 'end'. >> >> >> Makarius >> > >

**Follow-Ups**:**Re: [isabelle] Isabelle problem***From:*Makarius

**References**:**[isabelle] Isabelle problem***From:*Beta Ziliani

**Re: [isabelle] Isabelle problem***From:*Makarius

**Re: [isabelle] Isabelle problem***From:*Beta Ziliani

- Previous by Date: Re: [isabelle] Isabelle problem
- Next by Date: Re: [isabelle] Isabelle problem
- Previous by Thread: Re: [isabelle] Isabelle problem
- Next by Thread: Re: [isabelle] Isabelle problem
- Cl-isabelle-users June 2008 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