Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-07 03:07:46 -0800 (Fri, 07 Nov 2003)
Revision: 5079
Log message:

      - Added ".cmoz: .prla .prlb" dependency (with .prl* being optional) and added
      a requirement to build all .cmoz in .DEFAULT. This is necessary to make sure
      that .cmoz is properly updated after .prla is changed (by hand or via CVS).
      
      - Use the new reduceT in existing proofs, where appropriate.
      
      - Fixing itt's OMakefile - Alexei accidentally added the new itt_nequal to
      the PRINT_THEORIES instead of MPFILES.
      

Changes  Path
+4 -5 metaprl/OMakefile
+1 -1 metaprl/theories/itt/OMakefile
+2 -2 metaprl/theories/itt/itt_bisect.prla
+1 -1 metaprl/theories/itt/itt_bunion.prla
+2 -2 metaprl/theories/itt/itt_quotient_group.prla
+5 -5 metaprl/theories/itt/itt_record.prla
+3 -3 metaprl/theories/itt/itt_record_exm.prla
+2 -2 metaprl/theories/itt/itt_sortedtree.prla