Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-02 11:27:09 -0800 (Mon, 02 Jan 2006)
Revision: 8390
Log message:

      Added less ambiguous names for some of the refiner functions (for names
      like "eq", "hyps", "concl", etc.).
      
      Partial progress in Provable theorems, added a unification tactic.
      
      This commit is mainly just in case we have a power failure here--
      it is raining very hard.