Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-08 22:36:14 -0800 (Thu, 08 Jan 2004)
Revision: 5240
Log message:

      Itt_bool - added commutativity of band
      Itt_order - all properties up to strict/unstrict total order (decidable).
      Inverse order, conversion between strict-unstrict orders, their mutual
      relations, they preserve total orderness.
      lt_bool, le_bool, gt_bool and ge_bool are total orders over integers.
      Lots of trivial things are not proved but interesting theorems are.
      Record wrappers probably should be moved to a separate file.
      

Changes  Path
+4 -0 metaprl/theories/itt/itt_bool.ml
+431 -373 metaprl/theories/itt/itt_bool.prla
+352 -36 metaprl/theories/itt/itt_order.ml
+6 -18 metaprl/theories/itt/itt_order.mli
Added metaprl/theories/itt/itt_order.prla
Properties metaprl/theories/itt/itt_order.prla