Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-19 11:50:46 -0800 (Wed, 19 Nov 2003)
Revision: 5115
Log message:
******** WARNING - this commit breaks .prlb compatibility ******
******** Export all unsaved proofs to .prla before updating ****
- This commit fully implements the "infix" keyword that allows declaring
infix operators in MetaPRL files (with proper inheritance and scoping).
We used to have a partial implementation of it, but it did not work and was
not used.
- I also added the "suffix" keyword that is similar to the "infix" one.
- I changed the implementation of the standard infixes (such as thenT and thenC)
and the standard suffix (ttca) to use the proper mechanism instead of a filter
hack that defined all the infixes and suffixes globally as a part of the filter
code.