Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-16 20:13:40 -0800 (Mon, 16 Jan 2006)
Revision: 8488
Log message:

      NOTE: this is a moderate change to the internal way we handle
      resource annotations.
      
         - Resource arguments are now passed as labeled initial arguments to
           the annotation processor.  If you have an annotation processor
           that takes arguments, you define it as a function that takes
           the arguments and produces an annotation processor.
      
               val process_elim_resource_annotation :
                   ?options: elim_option list -> (term * (int -> tactic)) annotation_processor
      
         - The argument may be required or optional as desired.
      
         - Unlabeled arguments are relabeled as "options".
           Note that a function is allowed to take multiple arguments
           with the same label.
      
         - The annotation_processor and rw_annotation_processor types no
           longer require the first type argument.
      
      Changes to the "reduce" resource:
      
         - Added a ~select:<string> argument to the annotation processor
           that can be used to control when the rewrite
           is allowed.  By default, if the argument is not specified,
           the rewrite is always allowed.
      
         - You now need to use the wrap_reduce function when you add conversions
           manually (this is why so many files were changed in this update).
      
              let resource reduce +=
                 << foo >>, wrap_reduce reduce_foo
      
      Notes:
         - Since dT arguments are declared as optional, it is legal to
           write {| intro |} instead of {| intro [] |}.
      
         - We should allow other options to the reduce resource,
           including type inference, etc.
      
         - It is ok with me if we collect the reduce options into a list,
           like we do for dT.