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