Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-08-01 06:24:09 -0700 (Wed, 01 Aug 2001)
Revision: 3352
Log message:

      - Made sure conditional rewrites are added to toploop the same way the normal
      rules and rewrites are.
      - Added <<if ... then ... else ...>> term syntax macro (stands for iftenelse{ ; ; })
      - Proved and added to reduceC the reduction for ind with constant argument (as Brian
      requested). This reduction does everything except incrementing/decrementing the number
      (it will leave if as n + 1 or n - 1).
      - Fixed lt_bool reduction
      

Changes  Path
+18 -6 metaprl/doc/htmlman/user-guide/mp-terms.html
+28 -39 metaprl/filter/base/filter_prog.ml
+4 -0 metaprl/filter/base/term_grammar.ml
+126 -97 metaprl/theories/itt/itt_int_base.ml
+1 -1 metaprl/theories/itt/itt_int_base.mli
+0 -12 metaprl/theories/itt/itt_int_ext.ml