Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-02 21:13:35 -0800 (Wed, 02 Nov 2005)
Revision: 8082
Log message:

      Added string options.  These are like selT, but you need to use
      addOptionT or withOptionT.
      
      The differences with selT:
         1. The option is a string (perhaps it should be an opname?)
         2. A rule annotation can have multiple options using the
            [StringOption "foo"; StringOption "bar"] intro/elim
            argument.
      
      The addOptionT adds the option for the entire rest of the proof tree.
      The withOptionT adds it for a single tactic.
      The removeOptionT removes it for the rest of the proof tree.
      The withoutOptionT removes it for a single tactic.
      
      Unfortunately, the addOptionT isn't currently working.  Somewhere,
      it looks like proof annotations are getting cleared.  Looking
      into it.