Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-16 02:41:48 -0800 (Wed, 16 Nov 2005)
Revision: 8189
Log message:

      - Made multiplication a defined function (not an axiomatized one). Now we only
        have a single primitive rewrite for multiplication of numerals, everything
        else is derived.
      
      - Proved a bunch of itt_int_ext theorems that had not been proven yet.
      
      - Updated the parser so that <<-1>> is parsed as <<number[-1:n]>>, not
        <<minus{number[1:n]}}>>