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

      Experimenting with optimization.
      
        - Tried adding a checker to the normalizer to prevent it from
          running if the term is already in normal form.  This doesn't
          seem to help at all, so it is disabled.
      
        - Add a hack to try folding the equality into a membership
          before normalization.
      
             member{'T; 'e} <--> 'e = 'e in 'T
      
          This helps a lot, about 25% faster/shorter proofs.