Re: [isabelle] Isabelle problem



On Fri, 6 Jun 2008, Beta Ziliani wrote:

> theory ToyList
> imports PreList
> begin
> 
> is marked. But now mi context IS theory ToyList. And still nothing works:
> value "rev (True # False # [])"
> 
> throws
> *** Inner lexical error at: "# False # [])"
> *** At command "value".
> 
> like it didn't parse the theory.

At that point you do not have the datatype, only the content of the 
PreList theory.


	Makarius






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.