Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-02-21 09:29:16 -0800 (Thu, 21 Feb 2002)
Revision: 3506
Log message:

      When I removed .prlb and downloaded old .prla from CVS, mp does not showed
      "test2" rule and save() failed and reported incompletness of theory.
      So I had to remove .prla also and only then "test2" appeared.
      
      Another problem: some prefix of test2 conlusion appears red in emacs(???)
      
      And finally:
      cd"/";;
      ls"itt_int_arith";; - fails with:
      ls"itt_int_arith";;
      Refine error:
           ls: unrecognized option itt_int_arith
      Uncaught exception:
      Refine_error.MakeRefineError(TermType)(AddressType).RefineError("Shell", 1).
      
      
      and this last problem holds for any theory.
      

Changes	Path
+4525 -2803	metaprl/theories/itt/itt_int_arith.prla