Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-20 21:46:14 -0800 (Mon, 20 Feb 2006)
Revision: 8753
Log message:

      For hypothesis of the form "x: int", "x: nat", "x: BTerm", etc, where "x" does
      not occur anywhere, dT should simply thin out such a hypothesis, instead of
      trying to preform meaningless induction. This thinning should happen in
      AutoNormal.
      
      I've added a new option to elim annotations - annotating a rule with 
      "elim [ThinFirst thinT]" would cause dT to first try thinning out any matching
      hypothesis, and only apply the annotated rule when the corresponding variable
      is actually used somewhere.