Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-10 10:45:48 -0800 (Thu, 10 Nov 2005)
Revision: 8159
Log message:

      Proof checking is now completely decidable.
      
      A proof checker has the type
      
          ProofStep * ProofStepWitness -> bool
      
      where
      
          ProofStep == Sequent list * Sequent
          ProofStepWitness == BTerm list * BTerm list list
      
      I haven't converted Filter_reflection yet.