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
is marked. But now mi context IS theory ToyList. And still nothing works:
value "rev (True # False # )"
*** Inner lexical error at: "# False # )"
*** At command "value".
like it didn't parse the theory.
What I'm doing wrong???? :'(
On Fri, Jun 6, 2008 at 11:34 AM, Beta Ziliani <beta.ziliani at gmail.com>
> 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!"
> 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
>> > 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'.
This archive was generated by a fusion of
Pipermail (Mailman edition) and