Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-27 17:13:33 -0700 (Sun, 27 Jul 2003)
Revision: 4777
Log message:
Made the assumT's "assumption -> assertion" conversion algorithm a little
smarter.
| Changes | Path |
| +24 -5 | metaprl/refiner/reflib/match_seq.ml |
| +15 -6 | metaprl/refiner/reflib/match_seq.mli |
| +7654 -8880 | metaprl/theories/czf/czf_itt_bool.prla |
| +29 -42 | metaprl/theories/itt/itt_logic.ml |