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