Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-05 20:29:45 -0800 (Thu, 05 Jan 2006)
Revision: 8408
Log message:

      Re-added the Itt_hoas_sequent.bterm2_is_bterm rule.  However, this is
      not recommended because this kind of rule can break normal dT reasoning.
      
      Instead, I think these kind of rules are better accomplished with some
      kind of forward chaining (even the autoT kind should work fine, but I
      don't know how to enable it).
      
      Replaced the tactic in Pmn_core_terms.intro_term_TyAll with a terminating
      version.  Currently, expand_all () takes about 10sec for me.  Let me
      know if it doesn't terminate for you.
      
      Re-added pmn_core_terms.prla, so that you get the terminating tactics.
      Will remove this again once we all the proofs work.