Re: [isabelle] Isabelle problem
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
> theory ToyList
> imports PreList
> 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