[Logiweb] * proof of * reads *

Kasper H0st Frederiksen tofu at diku.dk
Mon May 30 10:32:10 CEST 2005


I have found out that in order to compile the following bit of proof:
---
"[ math khf theory proof of khf lemma one reads
 	arbitrary meta a cut meta a
    end math ]"
---

... I need to declare "PREASSOCIATIVE check: * proof of * reads *" in my 
bibliography. It is strange then that i _don't_ need to declare
"PREASSOCIATIVE check: arbitrary * cut *", infact if I add this line to my 
bibliography i get the error:

Frontend: parsing body
Symbol 85 of page 2 has the same name as symbol 85 of page 2
---

---
arbitrary meta a cut meta a
---
File page.pyk line 222 char 2:
Use of ambiguous construct
Submission aborted


Perhaps somone would lilke to comment on this.

-Kasper Frederiksen


More information about the Logiweb mailing list