Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-04 20:36:28 -0800 (Fri, 04 Nov 2005)
Revision: 8100
Log message:

      Added the (Annotate of tactic_arg * tactic_arg) proof step.  This
      addresses the problem with proof annotations being dropped.
      
      Proof files (.prlb and .prla) are defined to be backwards-compatible,
      but not forwards-compatible.