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

      Investigate a new plan of attack, where we prove theorems for all the
      common cases, say for mk_bterm up to arity 5.
      
      Place all the common cases in a "naive" BTerm normalizer, and run
      it before the general normalizer.
      
      This will continue to work, because it falls back to the general
      normalizer, but it should be faster if we have theorems for the common
      cases.
      

Changes  Path
+83 -2 metaprl/theories/itt/reflection/experimental/itt_hoas_normalize.ml
+4848 -876 metaprl/theories/itt/reflection/experimental/itt_hoas_normalize.prla