Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 23:04:08 -0800 (Wed, 15 Feb 2006)
Revision: 8717
Log message:

      - Added an AutoOK option to elim rule annotations. The rules marked with
        AutoOK will now be used by AutoNormal phase of autoT. The default for the
        elimination rules, as before, is to only use then in the AutoComplete phase.
      
      - Marked select elimination rules with AutoOK. In particular, the rules like
        and_elim and exists_elim are now marked with AutoOK, which eliminated the
        need to have a separate auto_logicT in autoT, which was a completely ad-hoc
        non-modular non-compositional way of decomposing certain hyps during the
        AutoNormal phase of autoT.
      
      - Improved the "relation" of the squash/unsuqash tactics and autoT. In
        particular, the unsquashing of the squash-stable conclusions will now happen
        during the AutoNormal phase (when the conclusion is _not_ squash-stable, it
        will only happen in the AutoComplete phase).
      
      This significantly speeds up status_all ( > 15%) and reduced the size of the
      PNM proofs (>20%).