Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-08 00:31:08 -0700 (Thu, 08 Jul 1999)
Revision: 2795
Log message:

      Changed the definition of compare_lt from (lt a b) to assert(lt a b).
      That allowed me to eliminate asserts from all the theorem statements and from most proofs.
      

Changes  Path
+42 -35 metaprl/theories/itt/itt_sort.ml
+1 -0 metaprl/theories/itt/itt_sort.mli
+22416 -3441 metaprl/theories/itt/itt_sort.prla