Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-18 13:46:14 -0800 (Sat, 18 Mar 2006)
Revision: 8936
Log message:

      Added support for interactive theorems.  This adds a reflected
      intro rule that corresponds to the theorem, but otherwise
      the rule is not considered to be part of the logic.
      
      Also added Pmn_core_terms_test2 that restates the theorem
      in Pmn_core_terms_test.  We should probably work on this one.