Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-06-01 14:29:49 -0700 (Thu, 01 Jun 2006)
Revision: 9238
Log message:

      Itt_hoas_lambda is obsolete.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-01 14:34:27 -0700 (Thu, 01 Jun 2006)
Revision: 9239
Log message:

      Proved that a logic is a sublogic of itself.
      Some comments

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-06-01 15:38:21 -0700 (Thu, 01 Jun 2006)
Revision: 9240
Log message:

      A few spelling fixes.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-02 13:07:47 -0700 (Fri, 02 Jun 2006)
Revision: 9244
Log message:

      Wrote more in reflection_quickref

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-02 13:58:32 -0700 (Fri, 02 Jun 2006)
Revision: 9245
Log message:

      Proved a lemma that is a partial case of transitivity (when Q=Top). 
      Some well-formedness assumption are probably redundant.

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-02 21:53:34 -0700 (Fri, 02 Jun 2006)
Revision: 9246
Log message:

      Make the vbind_in_bind2 theorem stronger

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-02 22:46:26 -0700 (Fri, 02 Jun 2006)
Revision: 9247
Log message:

      More on reflection_quickref

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-02 23:15:55 -0700 (Fri, 02 Jun 2006)
Revision: 9248
Log message:

      Remove an obsolete comment

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-02 23:56:53 -0700 (Fri, 02 Jun 2006)
Revision: 9249
Log message:

      itt_hoas_normalize does not need to depend on itt_hoas_sequent

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-03 01:03:50 -0700 (Sat, 03 Jun 2006)
Revision: 9250
Log message:

      Fixed an error

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-03 11:04:22 -0700 (Sat, 03 Jun 2006)
Revision: 9251
Log message:

      Simplify a proof

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-06-05 15:37:25 -0700 (Mon, 05 Jun 2006)
Revision: 9252
Log message:

      - Fixed spelling errors in documentation.
      - Enable spell-checking by default.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-06-05 16:58:23 -0700 (Mon, 05 Jun 2006)
Revision: 9255
Log message:

      (Group edit from last week committed by Aleksey.)
      
      First pass at cleaning up Itt_hoas_bterm - updated some comments, marked a
      number ot definitions and lemmas as private.
      
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-06-05 18:02:22 -0700 (Mon, 05 Jun 2006)
Revision: 9256
Log message:

      I am not sure what the "-$'(RM) ..." syntax used to do, but in 0.9.8 OMake no
      longer does anything special for this "-" and just complains that it can not
      execute "-rm", so I am removing the "-".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-06-06 14:11:26 -0700 (Tue, 06 Jun 2006)
Revision: 9259
Log message:

      Simplified the clean rules and made them 0.9.8-compatible.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-06-07 10:40:27 -0700 (Wed, 07 Jun 2006)
Revision: 9266
Log message:

      Updated the installation instructions (they were quite outdated). Also,
      commented out the Ensemble stuff, as the distributed prover will surely fail
      to compile.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-08 18:05:56 -0700 (Thu, 08 Jun 2006)
Revision: 9279
Log message:

      Wrote about rewriteC

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-09 17:59:35 -0700 (Fri, 09 Jun 2006)
Revision: 9283
Log message:

      Added two tactics: combineT combines several hypothesis in one and separateT is the opposite one. They are usefull for using induction on reflected proofs.  
      Rearanged things in Itt_struct2

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-09 18:13:54 -0700 (Fri, 09 Jun 2006)
Revision: 9284
Log message:

      Updated documentation

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-09 18:56:04 -0700 (Fri, 09 Jun 2006)
Revision: 9285
Log message:

      Added iforms: bind_list, subst_list for applying binding/substitution to the list of terms

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-06-16 11:01:48 -0700 (Fri, 16 Jun 2006)
Revision: 9332
Log message:

      Use @echo instead of println in .PHONY/editor/ml/done.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-16 12:22:43 -0700 (Fri, 16 Jun 2006)
Revision: 9334
Log message:

      Added a couple of rewrites about append in reduceC

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-16 13:34:51 -0700 (Fri, 16 Jun 2006)
Revision: 9337
Log message:

      BSequentCore{'n} was declared as a constant

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-20 15:37:25 -0700 (Tue, 20 Jun 2006)
Revision: 9350
Log message:

      Added new tactics:
       * reduceForallProdT rewrites hyps of the form all x: A*B*C... as all a:A.all b:B. all c:C...
      
       * varElimT : int -> tactic
       Eliminate a variable x using an equality x=t in A
      
       * allVarElimT
       Eliminate all possible variables.
      
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-20 15:44:41 -0700 (Tue, 20 Jun 2006)
Revision: 9351
Log message:

      Two more conversions:
      * reduce_vlistC :  Split the << vlist{| <J> |} >> into the standard form.
      
      * reduce_vflattenC : Split the << vflatten{| <J> |} >> into the append form.
      
      
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-20 15:54:57 -0700 (Tue, 20 Jun 2006)
Revision: 9352
Log message:

      Update the documentation

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-20 16:32:11 -0700 (Tue, 20 Jun 2006)
Revision: 9355
Log message:

      Added a relax rule.
      Also added a tactical doNotRelaxT
      
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-20 17:24:42 -0700 (Tue, 20 Jun 2006)
Revision: 9357
Log message:

      Made an error message more useful

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-20 20:18:57 -0700 (Tue, 20 Jun 2006)
Revision: 9360
Log message:

      Added new tactics (moveHypWithDependenciesT) that moves hypothesis when there are obscuring dependencies.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-20 22:20:43 -0700 (Tue, 20 Jun 2006)
Revision: 9364
Log message:

      Squiggle substitution rule should not change a name of the variable

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-06-21 05:36:22 -0700 (Wed, 21 Jun 2006)
Revision: 9365
Log message:

      Some documentation fixes.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-22 13:02:30 -0700 (Thu, 22 Jun 2006)
Revision: 9367
Log message:

      Changed the display form of append

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-22 13:05:44 -0700 (Thu, 22 Jun 2006)
Revision: 9368
Log message:

      Added ifthenelseT tactic to interface

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-23 12:02:20 -0700 (Fri, 23 Jun 2006)
Revision: 9375
Log message:

      Updated the documentation a littile bit

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-06-23 13:15:51 -0700 (Fri, 23 Jun 2006)
Revision: 9377
Log message:

      The fol theory is not a part of theories.pdf
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-06-23 13:42:12 -0700 (Fri, 23 Jun 2006)
Revision: 9378
Log message:

      Documentation fix.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-23 13:48:53 -0700 (Fri, 23 Jun 2006)
Revision: 9379
Log message:

      Use moveWithDependencesT instead of copyT in substT

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-23 16:18:15 -0700 (Fri, 23 Jun 2006)
Revision: 9383
Log message:

      Made simpleHypSubstT to be val instead of topval

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-23 17:01:06 -0700 (Fri, 23 Jun 2006)
Revision: 9384
Log message:

      Use moveWithDependencesT in varElimT

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-06-24 12:00:18 -0700 (Sat, 24 Jun 2006)
Revision: 9387
Log message:

      Documentation fix.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-26 14:40:37 -0700 (Mon, 26 Jun 2006)
Revision: 9399
Log message:

      Simplify substT

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-06-27 15:20:52 -0700 (Tue, 27 Jun 2006)
Revision: 9405
Log message:

      Updating the documentation (removing the link to htpp://cvs.metaprl.org that
      is about to become obsolete).