[kopylov] _ The theory ctt_markov _Constructive type theory with Markov_Mon Sep 19 02:53:37 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-53-37-816554000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-53-37-816554000-PDT.html[kopylov] ___ empty log message ____Mon Sep 19 02:53:40 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-53-40-674897000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-53-40-674897000-PDT.html[nogin] The function that was supposed to remove duplicate subgoals at the end of_Mon Sep 19 02:53:59 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-53-59-235693000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-53-59-235693000-PDT.html[nogin] Updated Itt_squash documentation._Mon Sep 19 02:54:00 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-00-793043000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-00-793043000-PDT.html[nogin] Fixed squash_resource annotations for empty types._Mon Sep 19 02:54:01 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-01-532094000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-01-532094000-PDT.html[kopylov] Some proofs in ctt_markov are simplified._Mon Sep 19 02:54:02 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-02-584574000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-02-584574000-PDT.html[nogin] _ For symbolic keywords, use tt instead of bf_Mon Sep 19 02:54:03 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-03-661292000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-03-661292000-PDT.html[kopylov] moveToConlT is fixed_Mon Sep 19 02:54:05 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-05-345448000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-05-345448000-PDT.html[kopylov] 1. I added new primitive rules__Mon Sep 19 02:54:06 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-06-020503000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-06-020503000-PDT.html[nogin] Prevent make from thinking there is a circular dependency._Mon Sep 19 02:54:28 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-28-906988000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-28-906988000-PDT.html[nogin] I am adding the current version of the resource problem and a description_Mon Sep 19 02:54:29 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-29-278601000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-29-278601000-PDT.html[lolorigo] fixed representation of level expression for mathbus_Mon Sep 19 02:54:29 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-29-815699000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-29-815699000-PDT.html[nogin] More specific details in Modules 2 and 3. Still need to finish 4 and write 5._Mon Sep 19 02:54:30 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-30-238876000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-30-238876000-PDT.html[kopylov] _Mon Sep 19 02:54:30 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-30-668009000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-30-668009000-PDT.html[nogin] Fixed Module 1, added lazyness wish _Problem 2.2_._Mon Sep 19 02:54:38 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-38-945396000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-38-945396000-PDT.html[nogin] I finished describing the code I propose_ still need to specify the_Mon Sep 19 02:54:39 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-39-385844000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-39-385844000-PDT.html[nogin] Finished the parsing part._Mon Sep 19 02:54:39 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-39-803769000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-39-803769000-PDT.html[kopylov] Start writing documentation for records._Mon Sep 19 02:54:41 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-41-374942000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-41-374942000-PDT.html[nogin] expand_all__ should go to next item on any exception, not just_Mon Sep 19 02:54:44 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-44-043082000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-44-043082000-PDT.html[nogin] Implemented object status inquiry__Mon Sep 19 02:54:45 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-45-642154000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-45-642154000-PDT.html[nogin] SOrt packages._Mon Sep 19 02:54:46 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-46-776447000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-46-776447000-PDT.html[nogin] Fixed a few proofs._Mon Sep 19 02:54:47 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-47-162787000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-47-162787000-PDT.html[nogin] _ A little better code for subgoal matching during proof expansion._Mon Sep 19 02:54:52 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-52-105993000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-52-105993000-PDT.html[nogin] Wrote Itt_struct.nthAssumT that is very similar to base theory nthAssumT, but_Mon Sep 19 02:54:53 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-53-214176000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-53-214176000-PDT.html[nogin] ASCII IO improvements for the case of a manually edited prla file containing_Mon Sep 19 02:54:59 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-59-253487000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-59-253487000-PDT.html[kopylov] _ Added tacticals whileProgressMT and untilFailMT_Mon Sep 19 02:54:59 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-59-713899000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-54-59-713899000-PDT.html[kopylov] _ Added the Itt_inv_typing theory that contain some inverse typing rule_Mon Sep 19 02:55:00 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-00-862970000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-00-862970000-PDT.html[nogin] Added support for the following syntax of resource improvement__Mon Sep 19 02:55:15 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-15-100546000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-15-100546000-PDT.html[kopylov] _ New tacticals_Mon Sep 19 02:55:18 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-18-996649000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-18-996649000-PDT.html[nogin] _ Changed the syntax of resource implementation. Now you no longer need to_Mon Sep 19 02:55:43 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-43-641772000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-43-641772000-PDT.html[nogin] _ Renamed andthenC __ thenC_Mon Sep 19 02:55:48 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-48-686410000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-48-686410000-PDT.html[nogin] Use byDefT in a few places._Mon Sep 19 02:55:56 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-56-276758000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-56-276758000-PDT.html[nogin] The redundant __resource_ suffix should not be used in resource names._Mon Sep 19 02:55:58 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-58-253085000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-55-58-253085000-PDT.html[kopylov] New tactics ans cnversionals are documented._Mon Sep 19 02:56:08 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-08-454941000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-08-454941000-PDT.html[kopylov] Fix an error_Mon Sep 19 02:56:08 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-08-973324000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-08-973324000-PDT.html[nogin] Got rid of annoying extra set _or _arg_ type argument in table functors._Mon Sep 19 02:56:09 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-09-350508000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-09-350508000-PDT.html[nogin] Resource annotations fix, thanks to Alexei K. for noticing this._Mon Sep 19 02:56:10 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-10-944958000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-10-944958000-PDT.html[nogin] Simplified some Camlp4 code._Mon Sep 19 02:56:11 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-11-347453000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-11-347453000-PDT.html[nogin] These were obsoleted by Term_match_table in _99 and are no longer in use._Mon Sep 19 02:56:12 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-12-285845000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-12-285845000-PDT.html[nogin] Converted remining .prlb_s in CVS into .prla_s._Mon Sep 19 02:56:12 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-12-934180000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-12-934180000-PDT.html[nogin] Made sure reflect_itt compiles._Mon Sep 19 02:56:32 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-32-697177000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-32-697177000-PDT.html[nogin] Removed the hack for old IO proof type _ I believe that_Mon Sep 19 02:56:33 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-33-963615000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-33-963615000-PDT.html[] This commit was manufactured by cvs2svn to create tag_Mon Sep 19 02:56:34 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-34-565001000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-34-565001000-PDT.html[nogin] ___ IMPORTANT_ before doing _cvs update_ see warning below ____Mon Sep 19 02:56:51 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-51-882977000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-51-882977000-PDT.html[nogin] Fixed a few proofs._Mon Sep 19 02:56:58 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-58-437625000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-58-437625000-PDT.html[nogin] _ Corrected precedences in Term_match_table _dforms, dT, etc_._Mon Sep 19 02:56:59 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-59-762479000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-56-59-762479000-PDT.html[nogin] _ Term_match_table seems to be finally doing the right thing._Mon Sep 19 02:57:00 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-00-241425000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-00-241425000-PDT.html[nogin] Fixed a problem with cond rewrites labels that I accidentally introduced earlier._Mon Sep 19 02:57:00 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-00-758161000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-00-758161000-PDT.html[nogin] Resource intermediate data type is irrelevant, so they are no longer required_Mon Sep 19 02:57:02 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-02-050710000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-02-050710000-PDT.html[kopylov] _ All rules in record theories are prooved _except some simple arith facts_._Mon Sep 19 02:57:03 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-03-127521000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-03-127521000-PDT.html[nogin] sub/sup should assume math mode._Mon Sep 19 02:57:28 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-28-372361000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-28-372361000-PDT.html[kopylov] _Mon Sep 19 02:57:28 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-28-762174000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-28-762174000-PDT.html[nogin] Updated SIL theory to a compilable state._Mon Sep 19 02:57:38 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-38-609892000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-38-609892000-PDT.html[nogin] Added a functionality to be able to limit JProver_s maximal multiplicity level._Mon Sep 19 02:57:39 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-39-490382000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-39-490382000-PDT.html[kopylov] Simplify primitive rules and improve tactics for elimination of intersection types._Mon Sep 19 02:57:40 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-40-358858000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-40-358858000-PDT.html[nogin] Added num_assums and nth_assums to Refine and Sequent._Mon Sep 19 02:57:55 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-55-167190000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-06/2005-09-19-02-57-55-167190000-PDT.html