Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-06 19:30:10 -0700 (Wed, 06 Jul 2005)
Revision: 7563
Log message:
This is a huge commit that is mostly no-op:
- Updated the standard preamble text to point to the correct location for the
documentation and to avoid mentioning Nuprl.
- Changed "Nuprl-Light" -> "MetaPRL" in a few places (amazingly, we still had
those).
- Split the Nuprl_font file into Mpfont and Mpsymbols.
- Protected a few display forms in ITT with a "doc docoff".