Re: [isabelle] Isabelle problem
Quick response! Thank you very much!
The thing is, I have in the buffer the hole theory, not only the part i put
in the mail. What I show was the part of the text marked by the error thrown
I think Proof General is driving me crazy, I will try to understand a little
bit more on what's happening, and use the command line. I don't understand
how to execute or see the result of nothing. I give up! Or the tutorial is
incomplete, or it assume some knowledge (and dough is not a tutorial), or
I'm a complete idiot, which is not something we can discard...
On Fri, Jun 6, 2008 at 12:10 PM, Makarius <makarius at sketis.net> wrote:
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and