[jyh] Proved the induction principle on derivations._Tue Nov 1 12:52:06 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-01-12-52-07-002334000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-01-12-52-07-002334000-PST.html[jyh] Rebuilt the FSub languages directly from BTerm._Tue Nov 1 20:01:17 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-01-20-01-17-667954000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-01-20-01-17-667954000-PST.html[jyh] Separate the judgments from the rules._Tue Nov 1 20:33:50 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-01-20-33-50-982732000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-01-20-33-50-982732000-PST.html[nogin] I am working on rewriting and simplifying MetaPRL core IO _ I want to change_Wed Nov 2 16:35:41 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-02-16-35-41-960382000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-02-16-35-41-960382000-PST.html[nogin] Working on the new IO. This commit mostly just rips apart the old code,_Wed Nov 2 16:43:12 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-02-16-43-12-207874000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-02-16-43-12-207874000-PST.html[jyh] Added string options. These are like selT, but you need to use_Wed Nov 2 21:13:37 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-02-21-13-37-557201000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-02-21-13-37-557201000-PST.html[jyh] Commented the code in Proof_boot that was removing all annotations_Thu Nov 3 10:38:24 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-10-38-24-867306000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-10-38-24-867306000-PST.html[nogin] Updated with Itt_dfun axioms instead of the Itt_rfun ones and Itt_pairwise_Thu Nov 3 16:47:43 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-16-47-43-119406000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-16-47-43-119406000-PST.html[nogin] _ Proved the nilSqequal rule _it used to be primitive_._Thu Nov 3 18:29:14 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-18-29-14-251749000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-18-29-14-251749000-PST.html[nogin] Defined the IO module for .cmiz_Thu Nov 3 21:01:48 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-21-01-48-911270000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-21-01-48-911270000-PST.html[jyh] _ Proof steps match only if the annotations match._Thu Nov 3 21:09:07 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-21-09-07-364586000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-21-09-07-364586000-PST.html[jyh] Added ty_exp_elim_slow for testing purposes._Thu Nov 3 21:35:59 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-21-35-59-978604000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-21-35-59-978604000-PST.html[nogin] Moving the closed branches out of the way._Thu Nov 3 22:00:19 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-22-00-19-552861000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-22-00-19-552861000-PST.html[nogin] Adding lm_set.ml to the list of files to be included in the _magic_ digest_Thu Nov 3 22:14:07 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-22-14-07-334065000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-22-14-07-334065000-PST.html[nogin] Exploring the _this takes too long_ example further. Simply running jproverT_Thu Nov 3 22:16:25 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-22-16-25-385016000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-03-22-16-25-385016000-PST.html[nogin] Relaxed a bit the test for _may be patterns_. If all occurrences of a second_Fri Nov 4 09:27:25 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-04-09-27-25-191049000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-04-09-27-25-191049000-PST.html[nogin] _ Updated the elimination rules for Union so that they better preserve binding_Fri Nov 4 10:05:21 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-04-10-05-21-315017000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-04-10-05-21-315017000-PST.html[jyh] Apparently we had forgotten to save string attributes to the IO proof_Fri Nov 4 14:07:17 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-04-14-07-17-510599000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-04-14-07-17-510599000-PST.html[jyh] Added the _Annotate of tactic_arg _ tactic_arg_ proof step. This_Fri Nov 4 20:36:30 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-04-20-36-30-355095000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-04-20-36-30-355095000-PST.html[jyh] Save the current version with structural induction while I_Sat Nov 5 13:20:44 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-05-13-20-44-929109000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-05-13-20-44-929109000-PST.html[jyh] Trying out the _well_formedness__based Fsub logic._Sat Nov 5 15:50:09 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-05-15-50-09-423019000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-05-15-50-09-423019000-PST.html[jyh] Added the _reflected_logic_ block, see Pmn_core_logic for an example._Sat Nov 5 20:41:00 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-05-20-41-00-833419000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-05-20-41-00-833419000-PST.html[nogin] Further _autoT is taking too long_ investagation _ in_Sat Nov 5 23:48:25 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-05-23-48-25-478489000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-05-23-48-25-478489000-PST.html[jyh] Returned to requiring wf of sequents, so that we don_t need wf_subgoals_Sun Nov 6 18:03:13 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-06-18-03-13-413948000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-06-18-03-13-413948000-PST.html[nogin] OMake should be checked out from the 0.9.6.x branch._Sun Nov 6 18:18:31 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-06-18-18-31-064991000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-06-18-18-31-064991000-PST.html[nogin] Minor fixes in the IO code. Still a long way to go._Sun Nov 6 22:35:46 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-06-22-35-46-454130000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-06-22-35-46-454130000-PST.html[nogin] _ env_arg.mli_ use self_documentary type names _e.g. _Arg.usage_msg_ instead_Mon Nov 7 01:14:47 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-01-14-47-951560000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-01-14-47-951560000-PST.html[nogin] Merged in the trunk changes _revisions 8080_8123___Mon Nov 7 01:23:10 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-01-23-10-070516000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-01-23-10-070516000-PST.html[kopylov] Added a theorem in the object theory._Mon Nov 7 17:49:13 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-17-49-13-796957000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-17-49-13-796957000-PST.html[nogin] _Issue 543_ Compute the full list of theories to build based on the_Mon Nov 7 19:11:18 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-19-11-18-353664000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-19-11-18-353664000-PST.html[jyh] Added a Boolean beq_bterm__t1_ _t2_ for alpha_equality_Mon Nov 7 20:07:22 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-20-07-22-289396000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-20-07-22-289396000-PST.html[nogin] Aleksey _ Alexei__Mon Nov 7 20:53:22 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-20-53-22-357020000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-20-53-22-357020000-PST.html[nogin] Centralized the nadling of the input search path._Mon Nov 7 23:36:43 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-23-36-43-819971000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-07-23-36-43-819971000-PST.html[nogin] Making sure the THEORYNAME/THEORYDESCR mechanism plays nicely with the new_Tue Nov 8 14:30:18 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-14-30-18-871670000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-14-30-18-871670000-PST.html[nogin] Tried making the THEORY_DEPENCIES code more rubust in presence of theory_Tue Nov 8 14:39:19 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-14-39-19-224898000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-14-39-19-224898000-PST.html[nogin] More consistent error messages for values in mk/config_Tue Nov 8 14:56:54 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-14-56-54-474656000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-14-56-54-474656000-PST.html[nogin] _THEORY_DEPENCIES_ __ _THEORY_DEPS_ _Oops, evils of too much cut_paste _ I_Tue Nov 8 15:04:58 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-15-04-58-633101000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-15-04-58-633101000-PST.html[jyh] This is like to be extremely contraversial._Tue Nov 8 15:23:45 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-15-23-45-579638000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-15-23-45-579638000-PST.html[jyh] The proof checkers are now _ProofStep __ bool_ instead of _ProofStep __ univ[1]_._Tue Nov 8 19:27:25 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-19-27-26-088887000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-19-27-26-088887000-PST.html[jyh] Update the filter to use beq_ProofStep._Tue Nov 8 19:43:29 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-19-43-29-632978000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-19-43-29-632978000-PST.html[jyh] Oops, I got a bit too aggressive on the Boolean proof checkers._Tue Nov 8 19:57:27 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-19-57-27-429864000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-08-19-57-27-429864000-PST.html[nogin] _ Made sure that documentation generator plays nicely with the new THEORY_DEPS_Wed Nov 9 00:19:57 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-09-00-19-57-155403000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-09-00-19-57-155403000-PST.html[nogin] Finished implementing the .cmiz API_Wed Nov 9 00:43:13 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-09-00-43-13-836079000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-09-00-43-13-836079000-PST.html[nogin] More TheoryDocument fixes._Wed Nov 9 04:55:04 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-09-04-55-04-778713000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-09-04-55-04-778713000-PST.html[nogin] Slight clarification._Wed Nov 9 16:14:19 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-09-16-14-19-208498000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-09-16-14-19-208498000-PST.html[jyh] Proof checking is now completely decidable._Thu Nov 10 10:45:53 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-10-10-45-53-362727000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-10-10-45-53-362727000-PST.html[jyh] Added the new explicit witness to Filter_reflection._Thu Nov 10 12:52:29 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-10-12-52-29-641171000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-10-12-52-29-641171000-PST.html[nogin] Added a rewrite lemma to reduce_ length_tail__l_ _n_ _ _n_Fri Nov 11 03:31:19 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-03-31-19-655516000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-03-31-19-655516000-PST.html[nogin] Trying to make _AutoComplete_ handling more efficient. In _AutoComplete_ mode_Fri Nov 11 05:10:59 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-05-10-59-469134000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-05-10-59-469134000-PST.html[nogin] Added a comment pointing to issue 549._Fri Nov 11 05:37:16 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-05-37-16-576028000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-05-37-16-576028000-PST.html[nogin] Adding omegaT to intro resource _with AutoComplete_ for inequality_Fri Nov 11 05:46:23 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-05-46-23-853873000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-05-46-23-853873000-PST.html[jyh] Proved some wf theorems._Fri Nov 11 11:44:01 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-11-44-01-155103000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-11-44-01-155103000-PST.html[kopylov] Some documentation on object theory_Fri Nov 11 12:11:04 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-12-11-04-935949000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-12-11-04-935949000-PST.html[kopylov] Proved that BTerm in U[i], and some other wf_theorems_Fri Nov 11 15:13:56 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-15-13-56-412270000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-11-15-13-56-412270000-PST.html[nogin] Added a moveHypT tactic _based on the Itt_struct.exchange rule_._Sat Nov 12 11:18:13 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-11-18-13-425555000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-11-18-13-425555000-PST.html[nogin] MP_DEBUG_spell fixes._Sat Nov 12 11:22:24 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-11-22-24-398117000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-11-22-24-398117000-PST.html[nogin] Restructured the file, making it more modular _IMHO__Sat Nov 12 15:47:43 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-15-47-43-507942000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-15-47-43-507942000-PST.html[nogin] When a negative _sequent context_ argument was too small _the absolute value_Sat Nov 12 16:20:23 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-16-20-23-826078000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-16-20-23-826078000-PST.html[nogin] Updated the irrefl_EliminationT tactic to work correctly with negative_Sat Nov 12 16:28:47 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-16-28-47-484278000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-16-28-47-484278000-PST.html[nogin] Wrote a simple program for merging two .prla files. This is__Sat Nov 12 17:29:05 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-17-29-05-939516000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-17-29-05-939516000-PST.html[jyh] Preparing to rename Itt_hoas_sequent_native to Itt_hoas_sequent._Sat Nov 12 19:06:03 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-19-06-03-344660000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-19-06-03-344660000-PST.html[jyh] Renamed Itt_hoas_sequent_native to Itt_hoas_sequent._Sat Nov 12 19:16:00 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-19-16-00-709940000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-12-19-16-00-709940000-PST.html[nogin] Updated the handling of matching of sequent contexts _sequent context_Mon Nov 14 04:09:26 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-14-04-09-26-373125000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-14-04-09-26-373125000-PST.html[nogin] Forgot to commit the updated filter_magic._Mon Nov 14 04:18:57 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-14-04-18-57-561605000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-14-04-18-57-561605000-PST.html[nogin] Fixed refiner_s term extraction._Mon Nov 14 05:47:50 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-14-05-47-50-388627000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-14-05-47-50-388627000-PST.html[nogin] Derived a slightly more convenient _in my and Alexei_s opinion_ induction rule_Tue Nov 15 01:38:42 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-15-01-38-42-025242000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-15-01-38-42-025242000-PST.html[nogin] A number of improvements in the .prla merging algorithm._Tue Nov 15 17:16:05 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-15-17-16-05-894160000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-15-17-16-05-894160000-PST.html[nogin] _ normalizeC should not call reduceC in the end, since reduceC might be doing_Tue Nov 15 23:26:20 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-15-23-26-20-016000000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-15-23-26-20-016000000-PST.html[nogin] _ Made multiplication a defined function _not an axiomatized one_. Now we only_Wed Nov 16 02:41:55 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-16-02-41-55-090541000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-16-02-41-55-090541000-PST.html[nogin] The .prla got corrupted. ___ Committing it again._Wed Nov 16 05:19:56 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-16-05-19-56-161518000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-16-05-19-56-161518000-PST.html[jyh] Partition the files into_Wed Nov 16 19:32:36 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-16-19-32-36-996497000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-16-19-32-36-996497000-PST.html[yegor] 1. Two minor optimizations for early detection of non_unifiable equations. Unfortunately, they do not help with the slow example in poplmark/naive._Thu Nov 17 21:48:20 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-17-21-48-20-121414000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-17-21-48-20-121414000-PST.html[nogin] Slight optimization of Yegor_s _quick incompatibility test_._Thu Nov 17 22:33:09 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-17-22-33-09-525889000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-17-22-33-09-525889000-PST.html[jyh] Added the context terms in extensions/meta_context_term_Tue Nov 22 12:15:44 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-22-12-15-44-431229000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-22-12-15-44-431229000-PST.html[jyh] Working on meta_implies. Still working on the meta_dT tactic._Tue Nov 22 17:10:49 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-22-17-10-49-527549000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-22-17-10-49-527549000-PST.html[jyh] The basic meta_dT works, but I haven_t corrected the _Tue Nov 22 17:41:52 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-22-17-41-52-447455000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-22-17-41-52-447455000-PST.html[jyh] Added the meta_cut rule._Tue Nov 22 18:07:51 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-22-18-07-51-866462000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-22-18-07-51-866462000-PST.html[jyh] Added the structural rules for the meta_logic, including cut and thinning._Tue Nov 22 19:55:15 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-22-19-55-15-829241000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-22-19-55-15-829241000-PST.html[jyh] Generalized the type of ML extract functions. The previous_Wed Nov 23 09:36:45 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-23-09-36-45-711537000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-23-09-36-45-711537000-PST.html[jyh] Minor changes. Meta_implies should depend on Meta_struct, not_Wed Nov 23 11:35:20 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-23-11-35-20-868450000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-23-11-35-20-868450000-PST.html[jyh] Added the minimal boilerplate for context induction._Wed Nov 23 12:20:42 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-23-12-20-42-610318000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-23-12-20-42-610318000-PST.html[jyh] Trivial changes while I work out a plan._Wed Nov 23 14:18:23 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-23-14-18-23-751608000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-23-14-18-23-751608000-PST.html[jyh] Added the TermMan.all_vars_info function. The Perl script isn_t_Wed Nov 23 18:07:42 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-23-18-07-42-107193000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-23-18-07-42-107193000-PST.html[nogin] Updating Refiner_debug to match the latest Jason_s changes._Wed Nov 23 20:33:26 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-23-20-33-26-440680000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-23-20-33-26-440680000-PST.html[jyh] Initial context induction tactics._Fri Nov 25 15:26:16 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-25-15-26-16-272630000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-25-15-26-16-272630000-PST.html[jyh] Theory rearrangement._Fri Nov 25 15:46:44 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-25-15-46-44-142888000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-25-15-46-44-142888000-PST.html[jyh] Deriving the sequent_ind reight reduction._Fri Nov 25 19:22:18 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-25-19-22-18-394099000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-25-19-22-18-394099000-PST.html[jyh] Proved right_reduction for sequent_ind_...__Sat Nov 26 08:06:52 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-08-06-52-026916000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-08-06-52-026916000-PST.html[jyh] Proved context thinning and context exchange._Sat Nov 26 09:30:06 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-09-30-06-440587000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-09-30-06-440587000-PST.html[jyh] Added some defined versions of sequent_ind_...__Sat Nov 26 12:05:51 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-12-05-51-721090000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-12-05-51-721090000-PST.html[jyh] Rename the derived terms._Sat Nov 26 12:08:27 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-12-08-27-020731000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-12-08-27-020731000-PST.html[jyh] Added the initial vector_list theory._Sat Nov 26 13:03:52 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-13-03-52-170097000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-13-03-52-170097000-PST.html[jyh] Ouch_ Term_ds had an unfortunate typo. This could potentially_Sat Nov 26 14:13:11 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-14-13-11-186484000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-14-13-11-186484000-PST.html[jyh] Considering reformulating recursive lists._Sat Nov 26 16:58:56 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-16-58-56-795799000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-16-58-56-795799000-PST.html[jyh] Proved basic theorems for vector lists._Sat Nov 26 17:27:27 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-17-27-27-525749000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-26-17-27-27-525749000-PST.html[jyh] Proved that the second phase of sequent reflection is well_formed._Sun Nov 27 14:45:07 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-27-14-45-07-476697000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-27-14-45-07-476697000-PST.html[jyh] Partial progress on the front_end to the sequent definition._Sun Nov 27 19:37:54 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-27-19-37-54-366879000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-27-19-37-54-366879000-PST.html[jyh] Proved the final wf goal._Mon Nov 28 11:10:11 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-28-11-10-11-053761000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-28-11-10-11-053761000-PST.html[jyh] Stated a provability theorem, just to see what it looks like._Mon Nov 28 12:58:01 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-28-12-58-01-543969000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-28-12-58-01-543969000-PST.html[nogin] Addressing some of the comments by the second reviewer._Mon Nov 28 18:56:01 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-28-18-56-01-287810000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-28-18-56-01-287810000-PST.html[nogin] Added couple of paragraphs to the end of the _Summary and Future Work__Mon Nov 28 19:25:51 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-28-19-25-51-816525000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-28-19-25-51-816525000-PST.html[nogin] Fixing a few typos_Mon Nov 28 19:29:21 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-28-19-29-21-956911000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-28-19-29-21-956911000-PST.html[nogin] HOSC paper_ Addressing another reviewer_s comment_Tue Nov 29 18:33:18 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-29-18-33-18-137732000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-29-18-33-18-137732000-PST.html[nogin] HOSC paper_ fixing couple of typos_Tue Nov 29 18:38:33 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-29-18-38-33-232606000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-29-18-38-33-232606000-PST.html[nogin] HOSC paper_ addressing couple of more reviewer_s comments_Wed Nov 30 03:25:30 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-03-25-30-254399000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-03-25-30-254399000-PST.html[jyh] Committing some half_completed work before we lose it. The_Wed Nov 30 08:15:37 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-08-15-37-317910000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-08-15-37-317910000-PST.html[jyh] Further cleanup._Wed Nov 30 08:18:39 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-08-18-39-118004000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-08-18-39-118004000-PST.html[nogin] HOSC paper_ _CloseRec is an administrative ter.m__Wed Nov 30 11:56:01 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-11-56-01-188995000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-11-56-01-188995000-PST.html[jyh] Added a section on the runtime._Wed Nov 30 12:30:40 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-12-30-40-889169000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-12-30-40-889169000-PST.html[jyh] More changes, added a reference to A_normal form._Wed Nov 30 14:12:44 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-14-12-44-862271000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-14-12-44-862271000-PST.html[nogin] HOSC paper_ spelling_Wed Nov 30 14:42:07 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-14-42-07-098850000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-14-42-07-098850000-PST.html[jyh] Recent changes._Wed Nov 30 14:53:40 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-14-53-40-312566000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-14-53-40-312566000-PST.html[jyh] Jason_s final copy._Wed Nov 30 17:23:09 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-17-23-09-332968000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-11/2005-11-30-17-23-09-332968000-PST.html