Re: [isabelle] Isabelle problem
On Fri, 6 Jun 2008, Beta Ziliani wrote:
> theory ToyList
> imports PreList
> is marked. But now mi context IS theory ToyList. And still nothing works:
> value "rev (True # False # )"
> *** 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and