Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-07 20:53:20 -0800 (Mon, 07 Nov 2005)
Revision: 8129
Log message:

      Aleksey & Alexei:
      
      - Simplified the induction axioms for integers and lists, deriving the
        original ones.
      
      - Annotated the induction rules for ints, nats, and lists with proper labels,
        increasing the list of labels that are considered to be "main" by thenMT.
      
      - Making progress re-verifying ITT Core axioms under pairwise functionality
        (but got stuck in Itt_int_ext, where the div_neg rule seems too suspicious).