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

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

Beta



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




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