Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-04 00:43:46 -0700 (Fri, 04 Aug 2000)
Revision: 3038
Log message:

      ensemble01.cs.cornell.edu -> cvs.metaprl.org
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-04 10:28:59 -0700 (Fri, 04 Aug 2000)
Revision: 3039
Log message:

      Even shorter URLs:
      http://cvs.metaprl.org:12000/cvsweb/~checkout~/meta-prl/doc/htmlman/... ->
      http://cvs.metaprl.org:12000/metaprl/...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-07 15:04:09 -0700 (Mon, 07 Aug 2000)
Revision: 3041
Log message:

      Removed several very old REDAME files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-09 16:54:39 -0700 (Wed, 09 Aug 2000)
Revision: 3042
Log message:

      Got rid of Itt_equal!member.
      ----------------------------
      
      Now the only way to represent membership in ITT is to use << equals{T;x;x} >>
      To avoid extra typing, this can be typed as << x IN T >> (note that "IN" has
      to be capitalized here, while in << x=x in T >> it has to be lowercase).
      
      I updated the rules and tactics approprially. I also updated itt_quickref.txt
      (Although I have not checked whether the original text was correct and if it was
      not, my modifications could also be incorrect).
      
      I reexpanded all the proofs. Most worked correctly, except for the following:
      - Some proofs were nonexistant or incomplete even before my changes.
      - Itt_fset is very outdated and would not expand without some major effort.
      - Many proofs in Itt_collection are broken because of heavy reliance on tatcics
      that need term arguments that were broken by the variable naming bug (BUGS 3.11).
      I am not sure whether it's the only problem with Itt_collection (probably not).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-10 16:10:47 -0700 (Thu, 10 Aug 2000)
Revision: 3043
Log message:

      Documented couple of problems with the build system.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-13 21:23:46 -0700 (Sun, 13 Aug 2000)
Revision: 3046
Log message:

      Fixed the display form order - now the newer display form takes priority over
      an older one instead of the other way around. This make it possible to overwrite
      a standard display form with a theory-specific one (for example, itt_sort overwrites
      the display form for Itt_list!list_ind).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-13 21:28:07 -0700 (Sun, 13 Aug 2000)
Revision: 3047
Log message:

      I changed the unhide rules according to hide{A} = squash{A} semantics.
      
      Alexei, can you take a look at my changes and see if you agree with them?
      Also, do we need more elimination rules for union and more introduction rules
      for intersection?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-16 00:29:04 -0700 (Wed, 16 Aug 2000)
Revision: 3048
Log message:

      Fixed some mess with dispaly forms. But we still need to implement mode generality,
      sets of modes (or at least something like mode[all except src] flag)
      and make sure that the modes are correct on all the dforms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-17 00:16:06 -0700 (Thu, 17 Aug 2000)
Revision: 3049
Log message:

      - Do not go to proof cache for non-interactive proof steps (Jason, do youu agree
      with this change to proof_boot)?
      
      - By default, do not print debugging messages from jall
      
      - When printing addresses, start numbering hyps from 1, not 0.
      
      - Added "rev" list revercing operation. We need to implement rewrites properly
      and/or add rewriting using equality in order to be able to prove the properties
      of list functions in some reasonable way.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-19 18:40:18 -0700 (Sat, 19 Aug 2000)
Revision: 3050
Log message:

      - I added my personal TODO file that contains a list of things
      that I am considering doing with/in/about/around MetaPRL
      
      - I fixed the display form modes in ITT!!!
      1) I added the except_mode[...] display form option. It is opposite
      to the mode[...] option. The main idea was to be able to say
      except_mode[src]
      2) I made sure all the display forms in ITT (and below it, except for
      Ocaml) are annotated with proper mode and except_mode options.
      3) I added (in one of the previous commits) the  set_dfmode
      command to MetaPRL toploop. Now  set_dfmode "src"  can be used
      to produce terms in a form suitable for cutting and pasting into
      .ml files and command line tactic arguments.
      4) I updated the documentation accordingly.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-21 22:48:22 -0700 (Mon, 21 Aug 2000)
Revision: 3051
Log message:

      More warnings on tutorial...
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-08-29 17:56:48 -0700 (Tue, 29 Aug 2000)
Revision: 3052
Log message:

      Two changes.
         1. expand () now does sloppy expansion, so that proofs
            can be replayed even if the goal of a proof has changed.
            This also means that proof copy/paste should work.
      
         2. I fixed up CZF.  This is a pretty cool set theory, where
            we get the usual ZF axioms (except excluded middle).  The
            normal things like numbers can be coded in the usual
            way, except we get decidability of number equality and
            other constructive ideas.  Reals can be coded with
            Dedekind cuts according to Aczel.  This theory is the
            basic set theory with just the axioms.  Before going on,
            it is probably a good idea to stratify the sets with
            levels, so we can formalize the notion of classes.
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 2000-08-31 22:05:44 -0700 (Thu, 31 Aug 2000)
Revision: 3053
Log message:

      1) Enable compilation under Debian
      
      2) enable "define" form in *.ml files (as well as *.mli files)