Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-21 11:45:31 -0800 (Tue, 21 Feb 2006)
Revision: 8766
Log message:

      This adds the simpleReduceT tactic to autoT on AutoNormal level.
      
      This noticeably speeds up the "status_all" and significantly reduces the size
      of reflection proofs:
      
        Expanding `intro_term_Apply':
        -Status: /pmn_core_terms/intro_term_Apply is a derived object with a complete proof (1 rule boxes, 16071 primitive steps)
        +Status: /pmn_core_terms/intro_term_Apply is a derived object with a complete proof (1 rule boxes, 9430 primitive steps)
        Expanding `intro_term_Lambda':
        -Status: /pmn_core_terms/intro_term_Lambda is a derived object with a complete proof (1 rule boxes, 37250 primitive steps)
        +Status: /pmn_core_terms/intro_term_Lambda is a derived object with a complete proof (1 rule boxes, 23894 primitive steps)