Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-17 19:59:44 -0800 (Fri, 17 Mar 2006)
Revision: 8931
Log message:

      For terms declared in the signature, say
      
          declare foo{...}
      
      also declare the proof-checking term in the reflected theory
      
          declare term_foo
      
      Long term, we have the issue of dealing with privately-declared
      terms.  Short-term, we will soon have the issue of dealing with
      privately-declared rules (which are our usual style).
      
      I'm not sure what to do, but perhaps we'll just declare the rules
      in the interface too for now.