Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-03 21:08:10 -0800 (Thu, 03 Nov 2005)
Revision: 8090
Log message:

      - Proof steps match only if the annotations match.
      - Removed annotation removal during IO squashing.
      - Expanded all proofs that produce warning messages,
        and re-exported them.
      
      Note, I believe I hit the weak-memo bug, or something like it
      during proof expansion, and I got crazy terms appearing in
      unrelated theorems:(  I believe I have re-fixed all those
      broken proofs.  check-status reports that all is well.