Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-08-13 15:27:12 -0700 (Sun, 13 Aug 2006)
Revision: 9494
Log message:

      On Win32, the OpenSSL libraries have been renamed.
      
      Be sure to escape the browser path on  Win32 (because
      it contains \ characters).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-08-15 11:10:45 -0700 (Tue, 15 Aug 2006)
Revision: 9500
Log message:

      Killing a debugging line that was accidentally committed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-08-20 17:28:08 -0700 (Sun, 20 Aug 2006)
Revision: 9505
Log message:

      Better "source file is shadowed by a stale binary file" error message.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-08-23 14:16:52 -0700 (Wed, 23 Aug 2006)
Revision: 9524
Log message:

      Gave an explicit definition to div and rem. Replaced all the relevant axiom
      with interactive rules and proved some (but not all) of them.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-08-23 16:31:14 -0700 (Wed, 23 Aug 2006)
Revision: 9526
Log message:

      Added TermOp.mk_string_dep0_dep0_dep0_term
      

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.