Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-17 23:44:07 -0800 (Tue, 17 Jan 2006)
Revision: 8503
Log message:

      *** WARNING : BREAKS BINARY COMPATIBILITY ***
      ***  Export your proofs before updating!  ***
      
      This adds a private/public flag to all the resource improvements (including
      annotations). The public improvements get inherited by ancestors, while
      private ones remain local to the current theory.
      
      Syntax: 
      
      private let resource += ...
      public let resource += ...
      
      interactive foo {| public intro [AutoMustComplete]; private intro [] |} ...
      
      The private/public flag is optional, "public" is assumed by default.
      
      Note: short of not breaking the existing code, this is completely untested.
      Will try testing tomorrow, unless Jason beats me to it.