[Logiweb] * proof of * reads *

[Martin Røpcke]

Hi,
I'm trying to use the construct

* proof of * reads *

and constantly get a NO INTERPRETATIONS error. The construct is defined on 
check page, and it is used on peano page, which does not refer to check. 
Nevertheless, the construct is used on peano page. How is that possible? 
I'm obviously missing something.

I get the error when including this:

"[ math
system prime s proof of mendelson lemma one eight reads
arbitrary meta b end line end math ]"

If I include "PREASSOCIATIVE check: * proof of * reads *" in my page, I 
get as far as end line, which then has no interpretation. Is there 
something I should read (or reread) in some page? Any advice will be much 
appreciated.

Regards,
Martin