Re: [isabelle] Isabelle problem



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
>>
>
>




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.