Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-23 21:12:16 -0800 (Mon, 23 Jan 2006)
Revision: 8586
Log message:

      Xin: I plan to merge the "branch" tomorrow, renaming all the numbered
         files, like Itt_hoas_sequent_term1.ml, back to their unnumbered
         versions.  This means I'll need to edit the .prla files.  If you
         commit your work, I'll edit your .prla too.  Otherwise, no big
         deal, we'll just edit it later.
      
      Finished off the proof for bsequent-wf forward chaining.  At this
      point, we're ready to reprove the Pmn_core_terms, which will require
      some tactic adjustments.