Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-14 18:57:55 -0800 (Mon, 14 Mar 2005)
Revision: 6922
Log message:
- Fixed a bug in parsing quotations within the <:doc< >> quotations.
- Added underline{'t} display form operator (which works correctly in HTML,
TeX and even PRL modes)
- Simplified and improved the display forms for the Base_reflection!bterm
sequents.
- Added a sample documenation to one of the ML rewrites in Base_reflection.