Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-02-21 09:29:16 -0800 (Thu, 21 Feb 2002)
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(???)
ls"itt_int_arith";; - fails with:
ls: unrecognized option itt_int_arith
and this last problem holds for any theory.