Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-08-24 12:04:44 -0700 (Thu, 24 Aug 2006)
Revision: 9531
Log message:

      Implemented support for "opqaue" definitions. An "opaque" definition can only
      be unfolded inside the theory that it's in.
      
      In order to use this, add the keyword "opaque" right after "define" in .ml
      file.
      
      Caveats:
       - Currently we only implement a "soft" restriction that can be easily
         circumvented. The "opaqueness" currently means that the rewrite will be
         added to the toploop resource as a "private" (not inheritable) entry. In
         other words, the definition unfolding conversion will only be visible in
         the toploop of the module that it's in, but one can easily make it visible
         outside of the module through ML.
       - Note that any resource annotation on an "opaque" definition will
         automatically be considered private (i.e. not be inherited by descendant
         theories).
      
      Todo:
       - The syntax is currently fragile - for example, for const definitions one
         has to use "define opaque const", while "define const opaque" will be
         rejected. We should allow an arbitrary ordering of these "flags".
       - We should consider enforcing the "opaqueness" of a definition via the
         refiner's sentinels. Alternatively, we might implement both the "soft opaque"
         restriction and the "hard opaque" one, but this will probably be
         unnecessary.
      
      P.S. I had to fix two HOAS proofs that refered to other module's definition
      for no good reason. Both proofs actually became simpler as a result,
      suggesting that the "opaqueness enforcement" is actually a good idea,
      
      P.P.S. Also, a number of proofs lost some (presumably unnecessary) primitive
      proof steps (probably because of the resource annotations becoming private -
      see the second caveat above). Again, seems like a good thing.