Re: [isabelle] Isabelle problem
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