Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-01 02:27:58 -0800 (Mon, 01 Dec 2003)
Revision: 5132
Log message:

      When changing a value of OCAMLDEP, we should _not_ rebefiner the scanner rule;
      instead we just need to add an extra dependency to the existing one.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-01 13:55:06 -0800 (Mon, 01 Dec 2003)
Revision: 5136
Log message:

      Adding the full bibliographical data for the ISSRE paper.
      
      Nathan, please dbl-check. Thanks!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-01 16:44:00 -0800 (Mon, 01 Dec 2003)
Revision: 5137
Log message:

      (bug 126) Use am empty command list (instead of the non-portable echo "")
      for dependenscy scanner in util.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-01 18:53:54 -0800 (Mon, 01 Dec 2003)
Revision: 5138
Log message:

      Uncommented several rules that were commented out because of the weak-memo problem.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-12-01 23:08:56 -0800 (Mon, 01 Dec 2003)
Revision: 5139
Log message:

      1. Committed Alexey's addition of thenTC.
      
      conv thenTC tac
       is a conversion that applies conv and then applies tac on additional
       subgoals (if any).
      
      2. Add new conversions:
      
      hypC n, revHypC n, assumC n, revAssumC n
      
      that replace t by s when  n-th hyp/assum is t~s (or s~t).
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-12-02 12:40:24 -0800 (Tue, 02 Dec 2003)
Revision: 5140
Log message:

      Start Dexter Kozen's theory of Kleene algebra with Tests.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-02 20:06:47 -0800 (Tue, 02 Dec 2003)
Revision: 5142
Log message:

      Added the full bibliography data for the TPHOLs cat B papers.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-12-03 11:25:39 -0800 (Wed, 03 Dec 2003)
Revision: 5143
Log message:

      Added associative and commutative resources.
      They are in experemental state right now and used only in KAT.
      
      Added a conversial
        subAssocC : int -> int -> conv -> conv
      subAssocC first length conv
      being apply to a_0 * a_1 * ... * a_n
      (where * is an associative operator)
      applies conv to a_first * ... * a_(first+lengt-1)
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-12-03 15:32:47 -0800 (Wed, 03 Dec 2003)
Revision: 5144
Log message:

      More on KAT
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-12-03 15:58:34 -0800 (Wed, 03 Dec 2003)
Revision: 5145
Log message:

      Some proofs in KAT
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-04 15:19:21 -0800 (Thu, 04 Dec 2003)
Revision: 5146
Log message:

      There is no need for an explicit dependency (which just creates a warning).
      

Changes by: Kamal Aboul-Hosn (kamal at cs.cornell.edu)
Date: 2003-12-04 16:06:23 -0800 (Thu, 04 Dec 2003)
Revision: 5147
Log message:

      Added axioms and theorems taken from the standard KAT library in KAT-ML.  These do not include boolean things yet.  Added kleene declaration to kat_terms.mli and kat_test to Makefile.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-12-04 21:05:43 -0800 (Thu, 04 Dec 2003)
Revision: 5148
Log message:

      KAT:
       - Move definitions of le,ge in kat_terms
       - Add wf rules in kat_terms
       - remove unneeded opens
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-05 20:46:40 -0800 (Fri, 05 Dec 2003)
Revision: 5149
Log message:

      Adding TPHOLs 2003 cat B bibtex entries.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-06 12:27:51 -0800 (Sat, 06 Dec 2003)
Revision: 5151
Log message:

      1.Renaming: rename_mul_add/rename_add_mul/as_additive were not delcared in .mli
      
      2.There was only theorem that G^car is type for groups, added for monoids
      
      3.Basic facts about rings. Additive group defined using renaming (see morph discussion),
      elimination rules still have to be fixed.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-06 22:01:10 -0800 (Sat, 06 Dec 2003)
Revision: 5152
Log message:

      1. rename{} was not declared in itt_record_renaming.mli
      2. typo in aabelg-intro rule fixed
      3. int_ring (ring of integers) declared and proved that integers is ring.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-07 07:52:36 -0800 (Sun, 07 Dec 2003)
Revision: 5154
Log message:

      Very preliminary version of fields.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-07 10:05:40 -0800 (Sun, 07 Dec 2003)
Revision: 5155
Log message:

      Two more files had rules commented out because of weak-memo problem.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-07 12:28:05 -0800 (Sun, 07 Dec 2003)
Revision: 5156
Log message:

      Declare the denerated files (to make sure dependencies are done properly).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-07 12:52:26 -0800 (Sun, 07 Dec 2003)
Revision: 5157
Log message:

      Minor clean-up.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-07 19:45:14 -0800 (Sun, 07 Dec 2003)
Revision: 5158
Log message:

      1. "car-0" renamed to car0
      2. Fixed definition of field (part about car0) according to Alexei's observation.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-07 19:56:45 -0800 (Sun, 07 Dec 2003)
Revision: 5159
Log message:

      1.Major (?) change in label-dependent tacticals semantics
        (thenMT, thenAT, thenPT, thenET, onAllMHypsT, tryOnAllMHypsT.
        Now they respect local assignments of labels rather than labels inherited
        from above.
      
      2.This implementation moved from itt_int_arith.
      
      3.onAllCumulativeHypsT, onAllMCumulativeHypsT, tryOnAllCumulativeHypsT,
        tryOnAllMCumulativeHypsT added. They also consider goals added during
        their execution.
      
      4.I didn't change thenLabLT, thenMLT and thenALT because they are not used
        anywhere (as far as I can tell) and change in their semantics is not that
        straightforward. I suggest to remove them at all.
      

Changes by: ( at unknown.email)
Date: 2003-12-07 19:56:45 -0800 (Sun, 07 Dec 2003)
Revision: 5160
Log message:

      This commit was manufactured by cvs2svn to create branch
      'unlabeled-1.2.2'.

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-07 20:11:26 -0800 (Sun, 07 Dec 2003)
Revision: 5161
Log message:

      Typp fixed (a<>b is not the same as a<>b in T).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-07 20:54:25 -0800 (Sun, 07 Dec 2003)
Revision: 5162
Log message:

      display form for int changed from mathbbZ to int
      
      int_ring renamed to Z
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-07 21:42:40 -0800 (Sun, 07 Dec 2003)
Revision: 5163
Log message:

      Unintentionally replaced AllHyps-tacticals with AllCumulativeHyps-tacticals.
      This fixes broken prove of itt_record_renaming/rename_exchange.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-07 23:09:09 -0800 (Sun, 07 Dec 2003)
Revision: 5164
Log message:

      Broken prove fixed. There was a "... thenWT autoT" deep under wf-subgoal.
      So this autoT processed not only local wf-subgoal but also main-subgoal.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-07 23:17:37 -0800 (Sun, 07 Dec 2003)
Revision: 5165
Log message:

      Some kind of problem fixed.
      I don't see any other problem in check-status log (it easy to miss a problem in this log).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-07 23:28:24 -0800 (Sun, 07 Dec 2003)
Revision: 5166
Log message:

      - Removed the seminars page (in made sense when all PRL stuff was done
      at Cornell, but not anymore).
      - Updated the people list (in particular, added Nathan to it)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-08 03:43:01 -0800 (Mon, 08 Dec 2003)
Revision: 5167
Log message:

      - Adding proofs for some of the rules added by Alexei in
      http://cvs.cs.cornell.edu:12000/commitlogs/metaprl/2003-11.html#03/11/14.20:24:29
      - Fixed a proof that was broken by 2001/07/02 18:34:20 commit.
      

Changes by: Kamal Aboul-Hosn (kamal at cs.cornell.edu)
Date: 2003-12-08 09:11:20 -0800 (Mon, 08 Dec 2003)
Revision: 5168
Log message:

      Added files corresponding to KAT-ML libraries
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-08 10:12:55 -0800 (Mon, 08 Dec 2003)
Revision: 5169
Log message:

      Clean up some weird code (which is currently unused anyway since it concerns
      ML rules).
      

Changes by: ( at unknown.email)
Date: 2003-12-08 10:12:55 -0800 (Mon, 08 Dec 2003)
Revision: 5170
Log message:

      This commit was manufactured by cvs2svn to create branch
      'unlabeled-1.4.2'.

Changes by: ( at unknown.email)
Date: 2003-12-08 10:12:55 -0800 (Mon, 08 Dec 2003)
Revision: 5171
Log message:

      This commit was manufactured by cvs2svn to create branch
      'unlabeled-1.8.2'.

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-12-08 14:32:37 -0800 (Mon, 08 Dec 2003)
Revision: 5172
Log message:

      Added version checking.
      Removed the unneeded dependency in refiner/rewrite/OMakefile.
      You will need to upgrade your omake to get the version right.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-12-08 16:04:14 -0800 (Mon, 08 Dec 2003)
Revision: 5173
Log message:

      
      Fixed a bug in assumC
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-11 22:11:21 -0800 (Thu, 11 Dec 2003)
Revision: 5174
Log message:

      1. wrap_terms added to null-refiner for postprocessing of tactic results
      2. implementation of "new" local semantics of thenMT, thenWT, etc moved to tactic_boot
      3. thenMLT and alike still not supported.
      
      Didn't check it with check-status. Aleksey, could you do it please?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-13 23:11:24 -0800 (Sat, 13 Dec 2003)
Revision: 5176
Log message:

      (bug 136) Do not strip off zeros from variable names.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-15 21:55:45 -0800 (Mon, 15 Dec 2003)
Revision: 5178
Log message:

      1.itt_ring - proved all theorems.
      
      2.itt_record - added a theorem on how recordOrt interplays with set.
      
      3.itt_field - original form of isField was incorrect, finally I added
      [i:l] to it because I say that car0 is equal to certain set.
      Still proof of isField_wf is incomplete yet and huge (it possibly
      means that itt_group*, itt_record* and itt_ring have imperfect design).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-16 14:14:51 -0800 (Tue, 16 Dec 2003)
Revision: 5179
Log message:

      refiner/refiner/refiner.ml is a generated file.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-16 15:51:13 -0800 (Tue, 16 Dec 2003)
Revision: 5180
Log message:

      We no longer need an explicit dependency on the "linear set" .cmi file.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-16 18:21:45 -0800 (Tue, 16 Dec 2003)
Revision: 5181
Log message:

      Merged shell_rule and shell_rewrite into a single module that does both.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-16 19:58:29 -0800 (Tue, 16 Dec 2003)
Revision: 5182
Log message:

      Adding support for a real check_all();;
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-16 20:56:35 -0800 (Tue, 16 Dec 2003)
Revision: 5183
Log message:

      forgot to rename prering_elim to prefield_elim when took template from itt_ring
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-16 21:28:25 -0800 (Tue, 16 Dec 2003)
Revision: 5184
Log message:

      Merging new-then_Lab_T-implementation branch to main trunk.
      thenMLT and alike still not supported.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-16 21:34:43 -0800 (Tue, 16 Dec 2003)
Revision: 5185
Log message:

      - Cache the dependency information.
      - A bit nicer printout in check_all();;
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-16 21:57:12 -0800 (Tue, 16 Dec 2003)
Revision: 5186
Log message:

      
      Sorry.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-16 22:08:37 -0800 (Tue, 16 Dec 2003)
Revision: 5187
Log message:

      Unintentional updated penetrated to cvs. Just for now rolling back to more consistent
      old definition of isField.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-16 22:56:37 -0800 (Tue, 16 Dec 2003)
Revision: 5188
Log message:

      Made the refiner.ml file ds/std switching use the macro preprocessor
      instead of having a generated file.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-16 23:53:14 -0800 (Tue, 16 Dec 2003)
Revision: 5189
Log message:

      More conforming header stuff for the MERLIN paper. Please dbl-check!
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-17 08:22:43 -0800 (Wed, 17 Dec 2003)
Revision: 5190
Log message:

      Proof of use_as_additive is complete now.
      

Changes by: ( at unknown.email)
Date: 2003-12-17 08:22:43 -0800 (Wed, 17 Dec 2003)
Revision: 5191
Log message:

      This commit was manufactured by cvs2svn to create tag
      'M_PAPER_MERLIN_2003_FINAL'.

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-17 22:23:20 -0800 (Wed, 17 Dec 2003)
Revision: 5192
Log message:

      On my way to make arithT depend only on proved rules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-18 00:10:31 -0800 (Thu, 18 Dec 2003)
Revision: 5193
Log message:

      (bug 141) Making sure omake gets the dependencies right:
      
      - ocamldep should not denerate .cmi/.cmo: .cmo dependencies when only .ml
      file is there, but no .mli is present. Instead, it should just generate the normal
      .cmi/.cmo: .cmi dependency (since .cmi is going to be build out of .ml)
      
      - omake can _not_ use "-I $(ROOT)/lib" since things will not be in lib yet at
      dependency scan time.
      
      - OCamlGeneratedFiles needs to be redefined for theory files to include .ppo
      dependencies.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-18 22:09:17 -0800 (Thu, 18 Dec 2003)
Revision: 5194
Log message:

      More proofs.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-19 22:02:08 -0800 (Fri, 19 Dec 2003)
Revision: 5195
Log message:

      1.More proofs
      2.reduce rule for distributivity:
      << ('a*@('b+@'c))>>,mul_add_Distrib_rw);
      
      replaced with
      << ('a*@('b+@'c))>>,((addrC [1] reduceC)thenC(tryC mul_add_Distrib_rw));
      
      we'll see how it'll work in check-status.
      The reason for change is simple if 'b and 'c are constants they should be
      contracted before distributivity but distributivity plays first in reduceC.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-20 20:41:12 -0800 (Sat, 20 Dec 2003)
Revision: 5196
Log message:

      1.Removed distributivity from reduceC.
      2.More proofs.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-20 21:42:32 -0800 (Sat, 20 Dec 2003)
Revision: 5197
Log message:

      All proofs except for the div/rem part are finished.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-20 21:47:40 -0800 (Sat, 20 Dec 2003)
Revision: 5198
Log message:

      All proofs are complete.
      This commit completes all proofs in itt_int* except for the div/rem part
      but div/rem are not used anywhere yet.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-21 14:41:47 -0800 (Sun, 21 Dec 2003)
Revision: 5199
Log message:

      Proof of int_ring_is_ring depended on presence of distributivity in reduce-resource.
      Fixed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-21 16:50:13 -0800 (Sun, 21 Dec 2003)
Revision: 5200
Log message:

      Fixing invalid backslash syntax in strings.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-21 18:53:36 -0800 (Sun, 21 Dec 2003)
Revision: 5201
Log message:

      This update fixes incorrect behaviour of arithT brought up by removal of distributivity from reduce-resources. This in particular fixes problem with itt_nat/int_div_rem.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-21 19:30:50 -0800 (Sun, 21 Dec 2003)
Revision: 5202
Log message:

      intro-resource for type(ext_equal) didn't work (as far as I can tell).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-21 22:17:44 -0800 (Sun, 21 Dec 2003)
Revision: 5203
Log message:

      1.isField is now defined using ext_equal for car0 (instead of equality in a universe).
      2.I believe isField_wf is complete modulo some basic interplay between renaming and
      recordTop. Or my be I just push into a deadend.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-22 19:22:39 -0800 (Mon, 22 Dec 2003)
Revision: 5204
Log message:

      
      1. Itt_grouplikeobj: isMonoid_wf2 added and proved,
                           I'd say that this form should be in intro-resource
                           instead of isMonoid_wf
      
      2. itt_record: recordOrtBisectIntro added and proved, recordOrt added to .mli
      
      3. itt_field: a couple of intermediate lemmas added.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-22 22:48:04 -0800 (Mon, 22 Dec 2003)
Revision: 5205
Log message:

      1.itt_subtype: transitivity of subtype stated and proved
      
      2.itt_record: recordOrtSetIntro - needless assumption removed
      
      3.itt_group: isCommutativity_wf add&proved though it's shaded by something else
      
      4.itt_ring: stronger introduction rules proved for AGroup and AAbelG
      
      5.itt_field: isField_wf is complete modulo invOrtRing and car0OrtRing which
      are complete modulo some problems with renaming
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-22 22:51:50 -0800 (Mon, 22 Dec 2003)
Revision: 5206
Log message:

      Better debug output added.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-23 09:07:41 -0800 (Tue, 23 Dec 2003)
Revision: 5207
Log message:

      Started (partial, etc) order theory.
      Currently we have to decide 3 issues:
      
      1.I define relation[i,rel] where rel is the label for particular relation, so you can have
      relation[i,<=], relation[i,>], etc. Do you think it's a good idea or variable labels are not well
      supported (or pain to use)
      
      2.I defined propositional relation, may be it is better to define boolean relations, may be both.
      Itt_int uses boolean relation as primitive one and propositional relations are "assert"s of booleans.
      
      3.One relation (say <) implies <=,>,>=, etc don't know how to make it nice.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-12-23 17:26:20 -0800 (Tue, 23 Dec 2003)
Revision: 5208
Log message:

      I have theory of relation structures of that includes preorders and equality relation.
      I need it for rbtrees.
      Currently this theory is a little bit mess and I did not prove anything.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-23 20:01:23 -0800 (Tue, 23 Dec 2003)
Revision: 5209
Log message:

      Added clarification how set_dfmode works, I write:
      It affects the output of functions that return terms immediately.
      For theory/proof listing you have to <TT>cd</TT> to "/" in order this change to take effect.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-23 20:32:38 -0800 (Tue, 23 Dec 2003)
Revision: 5210
Log message:

      Added several theorems about subtyping of records.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-23 20:33:22 -0800 (Tue, 23 Dec 2003)
Revision: 5211
Log message:

      1.Added itt_order to makefile
      2.Changed copyright notice
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-23 22:55:56 -0800 (Tue, 23 Dec 2003)
Revision: 5213
Log message:

      added:
       * "tac tatca" is a short for "tac thenAT tryT (completeT autoT)"
       * "tac twtca" is a short for "tac thenWT tryT (completeT autoT)"
       * "tac taa" is a short for "tac thenAT autoT"
       * "tac twa" is a short for "tac thenWT autoT"
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-23 23:02:49 -0800 (Tue, 23 Dec 2003)
Revision: 5214
Log message:

      Tryied new auto suffixes.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-24 22:20:53 -0800 (Wed, 24 Dec 2003)
Revision: 5215
Log message:

      Added two theorems(intro and elim style) about symmetry.
      Added two theorems that can replace equality in one type with equality in ext-equal type.
      May be last two rules should be added to elim-resource.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-25 23:01:25 -0800 (Thu, 25 Dec 2003)
Revision: 5216
Log message:

      1.Itt_subtype - added 2 elim-style versions of subtypeTransitive.
      2.Itt_ring,field - added 0<>1 condition to ring definition.
      It basically says that ring should have more than one element (that's why this
      conditon called isNonDegenerated).
      Actually I need this condition more for fields (to prove that 0 is not in car0)
      but anyway I don't think that "zero ring" is an "interesting" object.
      Please let me know if you think that this condition better be in field definition.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-26 22:35:19 -0800 (Fri, 26 Dec 2003)
Revision: 5217
Log message:

      Ext_equal: standard dest_ext_equal and other standard functions added.
      
      Subtype: Elim-style lemmas to prove that subterms are types.
      
      Struct3: replaceWithHypT, replaceWithRevHypT replace "x:T" with "x:S" when "T =e S" in hyps.
      

Changes by: Kamal Aboul-Hosn (kamal at cs.cornell.edu)
Date: 2003-12-29 09:43:14 -0800 (Mon, 29 Dec 2003)
Revision: 5218
Log message:

      Added reduce to appropriate rules.  The list is maintained in the file
      I use to convert from KAT-ML and adds the automatically in the conversion.
      Also started to define Hoare rules in the standard way with ifs and whiles
      and to let MetaPRL do the conversion on its own.