Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-03 21:02:01 -0800 (Fri, 03 Jan 2003)
Revision: 3976
Log message:

      - I added a list of authors to User Guid, Developr Guis and System Description.
      I came up with the lists based on quick browsing of CVS logs, so I might be mistaken,
      please let me know or feel free to fix yourself, if so.
      
      The current lists are:
      * Jason Hickey and Aleksey Nogin. MetaPRL System Description
      * Jason Hickey, Aleksey Nogin and Alexei Kopylov. MetaPRL User Guide
      * Aleksey Nogin and Vladimir Krupski. MetaPRL Developer Guide
      
      - Reorganized the "Hnn" headings - now only the main title page has H1, and the
      sections/subsections/subsubsections have H2-H4. Among other things this makes
      it look better in htmldoc'ed PDFs and PSs.
      
      - In the "simplified syntax" moved the "low priority terms closer to the end,
      it looked weird when the listings started with it.
      

Changes  Path
+1 -1 metaprl/doc/Makefile
+4 -2 metaprl/doc/htmlman/developer-guide/mp-developer-guide.html
+1 -1 metaprl/doc/htmlman/system/mp-auto-tactic.html
+1 -1 metaprl/doc/htmlman/system/mp-base-cache.html
+1 -1 metaprl/doc/htmlman/system/mp-base-syntax.html
+1 -1 metaprl/doc/htmlman/system/mp-base.html
+1 -1 metaprl/doc/htmlman/system/mp-chaining.html
+5 -5 metaprl/doc/htmlman/system/mp-conversionals.html
+1 -1 metaprl/doc/htmlman/system/mp-d-tactic.html
+4 -4 metaprl/doc/htmlman/system/mp-editor-imp.html
+7 -7 metaprl/doc/htmlman/system/mp-ensemble.html
+2 -2 metaprl/doc/htmlman/system/mp-filter.html
+1 -1 metaprl/doc/htmlman/system/mp-itt.html
+1 -1 metaprl/doc/htmlman/system/mp-ocaml.html
+6 -6 metaprl/doc/htmlman/system/mp-refine.html
+1 -1 metaprl/doc/htmlman/system/mp-refiner.html
+2 -2 metaprl/doc/htmlman/system/mp-rewrite.html
+4 -3 metaprl/doc/htmlman/system/mp-system.html
+1 -1 metaprl/doc/htmlman/system/mp-tactic.html
+6 -6 metaprl/doc/htmlman/system/mp-tacticals.html
+2 -2 metaprl/doc/htmlman/system/mp-terms.html
+1 -1 metaprl/doc/htmlman/system/mp-type-inf-rsrc.html
+5 -5 metaprl/doc/htmlman/user-guide/mp-axiom.html
+8 -8 metaprl/doc/htmlman/user-guide/mp-dform.html
+7 -7 metaprl/doc/htmlman/user-guide/mp-editor.html
+1 -1 metaprl/doc/htmlman/user-guide/mp-font.html
+3 -3 metaprl/doc/htmlman/user-guide/mp-modules.html
+4 -4 metaprl/doc/htmlman/user-guide/mp-rewrite.html
+34 -37 metaprl/doc/htmlman/user-guide/mp-terms.html
+5 -3 metaprl/doc/htmlman/user-guide/mp-user-guide.html