Re: [isabelle] Isabelle problem (*SOLVED*)



Sorry for being such a spammer, but I think that this mail can help another
guy.

The problem was that copy-paste from the tutorial is not a good idea,
because there are some characters (´ instead of ') that boiled Isabelle.
Still is missing in the tutorial that, when writting your theory, you have
to use it by pressing the "use" button. It sounds more obvious than it is, I
think.

Thank you Makarious for being pacient!

Cheers,
Beta

On Fri, Jun 6, 2008 at 12:17 PM, Beta Ziliani <beta.ziliani at gmail.com>
wrote:

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