[nogin] _ Derived a few Itt_union rules that used to be primitive _for no good_Wed Mar 1 10:51:16 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-10-51-16-844618000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-10-51-16-844618000-PST.html[nogin] Better usage of subtyping in nthHypT and dT._Wed Mar 1 12:54:27 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-12-54-27-187397000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-12-54-27-187397000-PST.html[nogin] When matching old subproofs with new subgoals during proof expansion, try_Wed Mar 1 18:37:23 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-18-37-23-831789000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-18-37-23-831789000-PST.html[nogin] Use the labels mechanism instead of the _SelectOption 5_ hack to control_Wed Mar 1 18:52:04 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-18-52-04-925025000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-18-52-04-925025000-PST.html[nogin] Be smarter when using subtyping in nthHypT and dT 0 _improves the code I_ve_Wed Mar 1 19:09:42 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-19-09-42-313546000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-19-09-42-313546000-PST.html[nogin] Added couple of nth_hyp annotations._Wed Mar 1 19:59:51 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-19-59-51-692937000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-19-59-51-692937000-PST.html[nogin] Added the missing wf condition to subtype_axiomFormation and fixed all the_Wed Mar 1 21:24:33 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-21-24-33-847976000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-21-24-33-847976000-PST.html[nogin] Thin out _0 in nat__Wed Mar 1 23:16:36 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-23-16-36-153874000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-01-23-16-36-153874000-PST.html[nogin] Use the nilSqequal lemma _ l _ [] in T List ___ l _ [] _ in _substT tactics_Thu Mar 2 00:12:58 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-00-12-58-739651000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-00-12-58-739651000-PST.html[nogin] Removed an unnecessary wf condition._Thu Mar 2 01:19:48 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-01-19-48-476626000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-01-19-48-476626000-PST.html[nogin] Removing an unnecessary wf condition._Thu Mar 2 01:44:00 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-01-44-00-278562000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-01-44-00-278562000-PST.html[nogin] Added _vflatten__ A __ ____ A_ to reduce._Thu Mar 2 02:28:24 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-02-28-24-580582000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-02-28-24-580582000-PST.html[nogin] Call simpleReduceT before using forwardT._Thu Mar 2 02:42:59 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-02-42-59-199906000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-02-42-59-199906000-PST.html[nogin] Removed some unnecessary wf conditions and replaced some of the proofs that_Thu Mar 2 10:12:30 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-10-12-30-283691000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-10-12-30-283691000-PST.html[nogin] Added TermAddr.null_address to TermAddr signature._Thu Mar 2 16:49:42 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-16-49-42-959832000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-16-49-42-959832000-PST.html[nogin] Exclude the obsolete directory from the build._Thu Mar 2 17:56:02 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-17-56-02-816225000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-17-56-02-816225000-PST.html[nogin] Xin_s recent commit made the weird caseAnalysis_7 lemma unnecessary, deleting._Thu Mar 2 18:36:59 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-18-36-59-917541000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-18-36-59-917541000-PST.html[nogin] Fixing a very nasty refiner bug, where the conditional rewrites were being_Thu Mar 2 18:45:28 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-18-45-28-693141000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-18-45-28-693141000-PST.html[nogin] All the Itt_list_sloppy theorems were valid_ I was able to fix all the proofs_Thu Mar 2 20:54:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-20-54-29-690677000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-20-54-29-690677000-PST.html[nogin] Added a missing wf condition, making the original proof replay._Thu Mar 2 21:04:09 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-21-04-09-732179000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-21-04-09-732179000-PST.html[nogin] My initial fix for the crw bug was not quite right either. Even this one is_Thu Mar 2 23:15:20 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-23-15-20-337756000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-02-23-15-20-337756000-PST.html[nogin] Fixed a few proofs that were broken by the _crw bug_ fix._Fri Mar 3 00:33:39 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-00-33-39-484898000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-00-33-39-484898000-PST.html[nogin] Tiny no_op code clean_up._Fri Mar 3 01:05:21 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-01-05-21-686779000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-01-05-21-686779000-PST.html[nogin] A little progress towards fixing the forward_chaining rules._Fri Mar 3 01:18:11 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-01-18-11-961299000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-01-18-11-961299000-PST.html[nogin] Adding the wf conditions that we will need to fix the proofs once the_Fri Mar 3 01:35:44 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-01-35-44-697300000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-01-35-44-697300000-PST.html[nogin] Itt_hoas_eta_Fri Mar 3 14:28:13 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-14-28-13-127935000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-14-28-13-127935000-PST.html[nogin] More accurate repeatT._Fri Mar 3 17:31:12 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-17-31-12-632481000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-17-31-12-632481000-PST.html[nogin] Optimized the Refine.msequent_alpha_equal function._Fri Mar 3 18:18:48 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-18-18-48-149866000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-18-18-48-149866000-PST.html[nogin] _Eta_converted_ the Itt_hoas_bterm_wf theory. Still have to _eta_convert_ the_Fri Mar 3 18:32:04 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-18-32-04-618465000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-18-32-04-618465000-PST.html[xiny] Made _t depend on _x in eta_bind and eta_bind1._Fri Mar 3 18:59:13 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-18-59-13-725401000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-18-59-13-725401000-PST.html[nogin] Minor optimization_Fri Mar 3 19:33:24 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-19-33-24-584964000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-03-19-33-24-584964000-PST.html[nogin] Rearranged things a bit_Sat Mar 4 21:59:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-04-21-59-01-771866000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-04-21-59-01-771866000-PST.html[nogin] Jason_s relarex HOAS works great__Sun Mar 5 09:57:33 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-09-57-33-743961000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-09-57-33-743961000-PST.html[nogin] Added a few items to the typeinf resource._Sun Mar 5 15:30:09 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-15-30-09-641978000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-15-30-09-641978000-PST.html[nogin] Making the Dtactic.intro_item type abstract._Sun Mar 5 15:37:30 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-15-37-30-855948000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-15-37-30-855948000-PST.html[nogin] Turned the intro_item type into a record type._Sun Mar 5 15:54:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-15-54-29-781672000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-15-54-29-781672000-PST.html[nogin] Implemented full fall_back for the intro resource. Now dT 0 will fall back to_Sun Mar 5 17:50:17 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-17-50-17-124142000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-17-50-17-124142000-PST.html[nogin] Previous commit had a typo, sorry._Sun Mar 5 17:51:33 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-17-51-34-005371000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-17-51-34-005371000-PST.html[nogin] Fixed couple of broken proofs. Most of the reflection proofs are now fully_Sun Mar 5 18:57:37 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-18-57-37-755366000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-18-57-37-755366000-PST.html[nogin] Fixed the remaining three broken reflection proofs. Now all the reflection_Sun Mar 5 19:40:34 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-19-40-34-168334000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-19-40-34-168334000-PST.html[nogin] Moving eta to obsolete, as we_ve managed to make things work without it._Sun Mar 5 19:44:00 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-19-44-00-090875000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-05-19-44-00-090875000-PST.html[xiny] Some modifications to make proving the elimination rule in reflect_pmn_core_terms a little easier._Thu Mar 9 13:44:51 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-09-13-44-51-552669000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-09-13-44-51-552669000-PST.html[xiny] Somehow, my previous commit can compile on my machine, but is uncomplilable by the cron. Try if this works._Thu Mar 9 14:56:31 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-09-14-56-31-111951000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-09-14-56-31-111951000-PST.html[jyh] Add the intial rule for multi_part elimination._Fri Mar 10 11:19:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-10-11-19-01-495698000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-10-11-19-01-495698000-PST.html[jyh] Define a predicate proof_check__r_ _assums_ _goal_ _witness_ that_Fri Mar 10 11:32:11 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-10-11-32-11-098815000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-10-11-32-11-098815000-PST.html[jyh] Add the initial SimpleStep case analysis rule._Fri Mar 10 12:10:17 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-10-12-10-17-956107000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-10-12-10-17-956107000-PST.html[nogin] Added a genHypT tactic._Fri Mar 10 17:00:41 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-10-17-00-41-064363000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-10-17-00-41-064363000-PST.html[jyh] Added the ProofCheck lemmas._Fri Mar 10 19:52:04 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-10-19-52-04-667806000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-10-19-52-04-667806000-PST.html[nogin] Squash is decidable when the type if decidable._Mon Mar 13 14:10:42 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-13-14-10-42-220736000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-13-14-10-42-220736000-PST.html[nogin] Need to use Lm_list_util.for_all2 instead of List.for_all2 when list lengths_Mon Mar 13 14:51:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-13-14-51-01-170419000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-13-14-51-01-170419000-PST.html[nogin] _ Changed the SimpleStep definition to use ProofCheck and the ValidStep_Mon Mar 13 15:34:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-13-15-34-01-608582000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-13-15-34-01-608582000-PST.html[jyh] Changes for compiling with strict quoting._Wed Mar 15 19:39:06 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-15-19-39-06-758767000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-15-19-39-06-758767000-PST.html[xiny] Added elimination rules for let_sovar and let_cvar, which made proving elim_pmn_core_terms much easier._Wed Mar 15 22:45:11 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-15-22-45-11-853455000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-15-22-45-11-853455000-PST.html[xiny] Some improvement_ made the elimination rule proof a little more general._Wed Mar 15 23:17:33 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-15-23-17-33-141092000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-15-23-17-33-141092000-PST.html[jyh] Last revision was a mistake _this is awk, not fsubst_._Thu Mar 16 12:08:27 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-16-12-08-27-484957000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-16-12-08-27-484957000-PST.html[jyh] MLDEBUG_PATH depends on project_directories, not dependencies._Thu Mar 16 16:43:54 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-16-16-43-54-991463000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-16-16-43-54-991463000-PST.html[jyh] Working on reflecting proper rules in Poplmark._Thu Mar 16 19:04:05 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-16-19-04-05-632901000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-16-19-04-05-632901000-PST.html[jyh] Added _hyp cases_ types. Probably soon to be modified, see message_Fri Mar 17 10:40:33 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-10-40-33-139878000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-10-40-33-139878000-PST.html[jyh] Use _Attempt _2_, which is equivalent to _Attempt _1_, but_Fri Mar 17 14:51:04 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-14-51-04-535615000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-14-51-04-535615000-PST.html[nogin] Added support for xquote0 on sequents _untested_._Fri Mar 17 18:33:28 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-18-33-28-884232000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-18-33-28-884232000-PST.html[nogin] Declare terms for rule names and the logic name in .cmiz _untested_._Fri Mar 17 19:09:25 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-19-09-25-634137000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-19-09-25-634137000-PST.html[jyh] Minor touchup on Aleksey_s fix._Fri Mar 17 19:33:21 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-19-33-21-314663000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-19-33-21-314663000-PST.html[jyh] For terms declared in the signature, say_Fri Mar 17 19:59:44 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-19-59-44-805803000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-19-59-44-805803000-PST.html[jyh] Starting work on reflecting proper rules. Will finish up_Fri Mar 17 20:35:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-20-35-29-640647000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-20-35-29-640647000-PST.html[xiny] Added a test file._Fri Mar 17 23:15:47 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-23-15-47-635203000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-17-23-15-47-635203000-PST.html[jyh] NOTE_ the magic number has changed. The change is_Sat Mar 18 10:04:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-10-04-01-461180000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-10-04-01-461180000-PST.html[jyh] _Sat Mar 18 13:11:15 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-13-11-15-128053000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-13-11-15-128053000-PST.html[jyh] Added support for interactive theorems. This adds a reflected_Sat Mar 18 13:46:15 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-13-46-15-733984000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-13-46-15-733984000-PST.html[jyh] Added the ProvableJudgment__logic_ _t_ that requires that the term_Sat Mar 18 15:03:12 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-15-03-12-046393000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-15-03-12-046393000-PST.html[jyh] Reflect the sequent declarations._Sat Mar 18 19:04:19 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-19-04-19-493943000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-19-04-19-493943000-PST.html[jyh] Working on display forms. Need to commit before I can move files._Sat Mar 18 20:21:55 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-20-21-55-539407000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-20-21-55-539407000-PST.html[jyh] Added _smart_ display forms for quoted terms._Sat Mar 18 20:54:03 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-20-54-03-906785000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-20-54-03-906785000-PST.html[jyh] Forgot to display variables correctly._Sat Mar 18 21:04:06 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-21-04-06-060929000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-18-21-04-06-060929000-PST.html[jyh] Generate the reflected interface file reflect_foo.ppi from_Sun Mar 19 09:42:26 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-19-09-42-26-925286000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-19-09-42-26-925286000-PST.html[jyh] Made some progress proving wf for elimination_style rules._Sun Mar 19 12:28:06 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-19-12-28-06-120835000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-19-12-28-06-120835000-PST.html[jyh] Half_finished theorems for proving_Mon Mar 20 09:45:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-20-09-45-01-218310000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-20-09-45-01-218310000-PST.html[nogin] Adding detection of stale binaries in directory that no longer has sources_Mon Mar 20 17:53:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-20-17-53-01-018078000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-20-17-53-01-018078000-PST.html[jyh] Almost done proving the nth_prefix lemma. Grinding through the_Mon Mar 20 21:02:34 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-20-21-02-34-128731000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-20-21-02-34-128731000-PST.html[nogin] The ge_elim resource options should be optional._Fri Mar 24 16:02:21 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-24-16-02-21-424200000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-24-16-02-21-424200000-PST.html[nogin] Couple of small lemmas_Fri Mar 24 16:07:59 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-24-16-07-59-371804000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-24-16-07-59-371804000-PST.html[nogin] Use relaxed reasoning in proofRuleAuxWFT tactic._Fri Mar 24 17:56:35 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-24-17-56-35-871397000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-24-17-56-35-871397000-PST.html[nogin] FOL should be using nth_hyp._Sat Mar 25 14:22:14 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-25-14-22-14-254710000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-25-14-22-14-254710000-PST.html[nogin] Minor_ proactively normalize BTerm__n __ 0 _ and CVar__n __ 0__Sat Mar 25 14:24:30 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-25-14-24-30-432691000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-25-14-24-30-432691000-PST.html[xiny] Made some progres on the nth_prefix lemma. Now it remains to prove bind_subst_nth_prefix_wf_aux0_ unfortunately, I couldn_t figure out how. bind_substl_nth_prefix_nth_suffix and bind_substl_nth_prefix can be ignored._Sat Mar 25 14:48:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-25-14-48-01-203703000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-25-14-48-01-203703000-PST.html[jyh] Proved a bunch of theorems about well_formedness of_Mon Mar 27 08:59:37 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-27-08-59-37-553620000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-27-08-59-37-553620000-PST.html[jyh] More progress on wf theorems._Mon Mar 27 22:07:43 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-27-22-07-43-746762000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-27-22-07-43-746762000-PST.html[xiny] Added some lemmas. Itt_hoas_proof_ind.provable_sub is unfinished yet._Mon Mar 27 23:31:03 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-27-23-31-04-000486000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-27-23-31-04-000486000-PST.html[jyh] Almost finished with the lemmas for the elim_style rules,_Wed Mar 29 07:40:56 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-29-07-40-56-346920000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-29-07-40-56-346920000-PST.html[xiny] Finally proved the lemmas about SubLogic._Wed Mar 29 15:31:00 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-29-15-31-00-025650000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-29-15-31-00-025650000-PST.html[nogin] In assumption_Wed Mar 29 19:11:39 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-29-19-11-39-331770000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-29-19-11-39-331770000-PST.html[nogin] _Re_ Rev 8943_ Minor proof simplification._Wed Mar 29 19:58:56 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-29-19-58-56-146041000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-29-19-58-56-146041000-PST.html[jyh] This finishes the intro forms of elimination_style rules. There is_Wed Mar 29 22:21:16 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-29-22-21-16-841465000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-29-22-21-16-841465000-PST.html[nogin] Added limited fallback to reduceC. ReduceC used to only try the very firts_Thu Mar 30 00:37:47 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-00-37-47-825027000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-00-37-47-825027000-PST.html[nogin] Small optimization._Thu Mar 30 02:38:53 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-02-38-53-710290000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-02-38-53-710290000-PST.html[nogin] _ Rewrote the forward_chainer__Thu Mar 30 05:17:41 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-05-17-41-260437000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-05-17-41-260437000-PST.html[nogin] Small optimization._Thu Mar 30 06:22:40 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-06-22-40-502766000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-06-22-40-502766000-PST.html[nogin] Thin some _useless_ hyps during forward chaining._Thu Mar 30 06:51:46 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-06-51-46-282369000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-06-51-46-282369000-PST.html[nogin] Proactively run simpleReduceC on all the subgoals that forward chainer_Thu Mar 30 11:03:18 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-11-03-18-481974000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-11-03-18-481974000-PST.html[nogin] Use options instead of exceptions in get_with_arg/get_with_args/get_univ_arg_Thu Mar 30 13:52:13 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-13-52-13-605820000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-13-52-13-605820000-PST.html[nogin] Adding extra elimination rules for _all i_ Index_l_. P[i]_ for the cases when_Thu Mar 30 14:10:11 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-14-10-11-262424000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-14-10-11-262424000-PST.html[nogin] Trivial no_op._Thu Mar 30 14:54:43 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-14-54-43-239139000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-14-54-43-239139000-PST.html[nogin] Minor optimization._Thu Mar 30 15:30:41 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-15-30-41-011624000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-15-30-41-011624000-PST.html[kopylov] Proved two missing elimination rules for sequents with non_zero depth_Thu Mar 30 20:02:39 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-20-02-39-502770000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-20-02-39-502770000-PST.html[nogin] Fixed a few of the corner cases in the forward chainer._Thu Mar 30 21:33:38 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-21-33-38-085386000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-30-21-33-38-085386000-PST.html[nogin] Small follow_up to my previous commit_Fri Mar 31 05:36:41 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-31-05-36-41-511333000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-31-05-36-41-511333000-PST.html[nogin] Implemented one of the elimination tactics._Fri Mar 31 12:07:26 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-31-12-07-27-000285000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-31-12-07-27-000285000-PST.html[xiny] Added some forward rules. Now the test rule in _pmn_core_terms_test_ is almost proved except for the _base_theory_ subgoal._Fri Mar 31 17:02:31 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-31-17-02-31-666683000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-31-17-02-31-666683000-PST.html[kopylov] Changed definiton of Sequent__d_. Now the argument of the sequent from Sequent_d_ must have the depth d._Fri Mar 31 17:04:16 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-31-17-04-16-902314000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-31-17-04-16-902314000-PST.html[nogin] The forward_chaining rules for equality should not have high priority_Fri Mar 31 17:27:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-31-17-27-29-312052000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-31-17-27-29-312052000-PST.html[xiny] Rearranged some rules._Fri Mar 31 17:33:05 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-31-17-33-05-749775000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-03/2006-03-31-17-33-05-749775000-PST.html