[Logiweb] * proof of * reads *

[Klaus Ebbe Grue]

Hi Martin and Ole,

You state in a number of e-mails that "* proof of * reads *" is defined on 
the check page. But it is defined on the base page.

To see this, do as follows:
Look up the base page. Then navigate to Dictionary->Pyk. Then do a "search 
on this page" for "* proof of * reads *". There you find a line saying
   589 3 * proof of * reads *
which indicates that symbol 589 of the base page has arity 3 and pyk name 
"* proof of * reads *". That proves that the base page defines a "* proof 
of * reads *" construct. Repeating the above for the check page reveals 
that the check page defines no "* proof of * reads *" construct.

I am not sure I understand what the problem with "* proof of * reads *" 
is, but I hope it helps to know that it comes from the base page.

Klaus
-------------- next part --------------
_______________________________________________
Logiweb mailing list
Logiweb at diku.dk
http://miming.diku.dk/mailman/listinfo/logiweb
(Web access from inside DIKUs LAN only)