Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-17 13:39:18 -0800 (Tue, 17 Jan 2006)
Revision: 8494
Log message:

      Changes to options:
      
         - Options are now based on opnames, so that we don't get
           accidental collisions between unrelated theories.
      
         - The tactic_arg options are OptionAllow and OptionExclude.
           So
      
              # Allow rules labeled with the given opname
              withAllowOptionT : term -> tactic -> tactic
      
              # Exclude rules labeled with the given opname
              withExcludeOptionT : term -> tactic -> tactic
      
           To make this work, we need to extend option annotations
           for rules.  Not done yet.
      
         - The Top_options.select resource can be used to specify
           default options for a theory.
      
           [Ping Aleksey]  I get confused by Mp_resource.  Currently,
           theory-local resources are pruned during close_theory.
           I don't know if this works.