Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-02 17:18:37 -0700 (Fri, 02 Jun 2000)
Revision: 3002
Log message:

      Wrote a section on MetaPRL exception-handling conventions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-02 17:18:53 -0700 (Fri, 02 Jun 2000)
Revision: 3003
Log message:

      .
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2000-06-03 03:46:57 -0700 (Sat, 03 Jun 2000)
Revision: 3004
Log message:

      Small correction in term_core variants
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-03 10:33:06 -0700 (Sat, 03 Jun 2000)
Revision: 3005
Log message:

      Removed some of the junk that Netscape added.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-04 18:48:17 -0700 (Sun, 04 Jun 2000)
Revision: 3006
Log message:

      Define type inference types only once, not in 5 places.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-08 04:55:06 -0700 (Thu, 08 Jun 2000)
Revision: 3007
Log message:

      Smarter type inference algorithm capable of doing things like
      
      # ti <<lambda{x.spread{'x;u,v.it}}>>;;
      - : Refiner.Refiner.Refine.term = x:(Top X Top) --> Unit
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-09 12:31:49 -0700 (Fri, 09 Jun 2000)
Revision: 3008
Log message:

      Added iff handling for Jprover and Barber example
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-09 15:15:36 -0700 (Fri, 09 Jun 2000)
Revision: 3009
Log message:

      Small Jprover<->MetaPRL interface fix - do not thin out universal
      quantifier on instantiation.
      

Changes by: Stephan Schmitt (sschmitt at sapient.com)
Date: 2000-06-09 18:08:48 -0700 (Fri, 09 Jun 2000)
Revision: 3010
Log message:

      
      Documented Example File, Bye guys
      

Changes by: Stephan Schmitt (sschmitt at sapient.com)
Date: 2000-06-09 18:10:41 -0700 (Fri, 09 Jun 2000)
Revision: 3011
Log message:

      
      Overview documentation and literatur citations, Bye guys :)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-11 14:15:38 -0700 (Sun, 11 Jun 2000)
Revision: 3012
Log message:

      let variable = expression in
         code
      
      is OK.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-12 15:05:11 -0700 (Mon, 12 Jun 2000)
Revision: 3013
Log message:

      Added gen_prover that Stephan forgot to commit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-12 23:16:19 -0700 (Mon, 12 Jun 2000)
Revision: 3014
Log message:

      I wrote a proof tree normalization that tries to eliminate unnecessary nodes
      in the proof tree and makes "deep" proof browsing much more
      plesent.
      
      Currently this is probably a little inefficient since it' too eager and
      the results are not always saved. To fix this, we'll need to make Tactic_boot extracts
      mutable so that we could do normalization (and other operations) properly lazily.
      
      Other small changes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-14 16:15:39 -0700 (Wed, 14 Jun 2000)
Revision: 3015
Log message:

      I reformatted the TODO file from Emacs "outline" mode to a numbered text file.
      We want to have numbers so that we can refer to items.
      
      When items are added to or removed from BUGS and TODO files, we should not do
      any renumbering to make sure the numbers stay the same.
      
      Fixed a small problem with ITT <-> Jprover interface.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-14 17:15:03 -0700 (Wed, 14 Jun 2000)
Revision: 3016
Log message:

      Numerous updates.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-21 15:05:17 -0700 (Wed, 21 Jun 2000)
Revision: 3019
Log message:

      Changes I've made at CADE: Further prof browsing improvements and others.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-29 14:13:29 -0700 (Thu, 29 Jun 2000)
Revision: 3020
Log message:

      assumT shouldn't run assertT when the conclusion is already what we want.