[Logiweb] Diagnose: Reference to unproved lemma - Solved

Kasper H0st Frederiksen tofu at diku.dk
Thu Jun 30 14:10:29 CEST 2005


Found it!
Turns out I was using "axiom a four" instead of "axiom prime a four". I 
replased this and it solved the problem.

-Kasper Frederiksen


On Thu, 30 Jun 2005, Martin Røpcke wrote:

> I had the same problem once. To locate the error, which I knew would be in 
> the last proof I had worked on, I deleted (as a comment) the last line and 
> made an error in the proof. It helped me know which lemma I was refering to. 
> Don't know if it can help.
>
> Regards,
> Martin
>
>
>
> On Thu, 30 Jun 2005, Kasper H0st Frederiksen wrote:
>
>> I am "suddenly" getting the diagnose
>> Reference to unproved lemma
>> but it dosn't tell me which lemma or where.
>> 
>> Could you please help me find the error.
>> 
>> I have uploaded the page to
>> http://www.diku.dk/~grue/logiweb/20050502/home/tofu/Reference-to-unproved-lemma/fixed/
>> 
>> -Kasper Frederiksen
>> _______________________________________________
>> Logiweb mailing list
>> Logiweb at diku.dk
>> http://miming.diku.dk/mailman/listinfo/logiweb
>> (Web access from inside DIKUs LAN only)
>> 
>
> Mvh
> Martin
>
> "I'm a great believer in luck and I find the harder I work,
> the more I have of it."
> Thomas Jefferson
>



More information about the Logiweb mailing list