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


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.