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 |