Cytowanie Adam Naumowicz <adamn@math.uwb.edu.pl>: ...
PYTHTRIP, for example, and try to verify it, I get the same *4 error. This makes me suspect that the assertion can never be accepted without explicit reference to the definition. Is this true?The registration mechanism only that works on adjectives cannot be used to infer the 'in' predicate. It would, of course, be possible to build it into the requirements directive, but the gain is relatively small as references to ORDINAL1:def 13 are not so frequent.
3261 in MML. Most of it, I believe, may be eliminated. Regards, Andrzej