[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