[jyh] Some intermediate results._Thu Dec 1 14:12:01 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-01-14-12-01-943480000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-01-14-12-01-943480000-PST.html[jyh] Some intermediate results._Thu Dec 1 18:43:53 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-01-18-43-53-029394000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-01-18-43-53-029394000-PST.html[jyh] Sorry about moving all files in theories/itt/extensions to_Fri Dec 2 20:39:19 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-02-20-39-19-470460000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-02-20-39-19-470460000-PST.html[jyh] Saving partial work._Fri Dec 2 20:44:55 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-02-20-44-55-212357000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-02-20-44-55-212357000-PST.html[nogin] Made _itt/extensions_ into a _virtual_ theory and made sure MetaPRL with_Sat Dec 3 14:10:24 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-03-14-10-24-453645000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-03-14-10-24-453645000-PST.html[nogin] Change the parse_time representation of the _default context dependencies_ to_Sat Dec 3 20:00:29 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-03-20-00-29-517848000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-03-20-00-29-517848000-PST.html[nogin] Improving the prlcomp function._Sat Dec 3 20:15:09 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-03-20-15-09-143550000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-03-20-15-09-143550000-PST.html[jyh] Added a theory of _sloppy_ or _lazy_ lists. The intent is_Sun Dec 4 09:29:30 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-04-09-29-30-612367000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-04-09-29-30-612367000-PST.html[nogin] Another _itt/extensions __ /itt/extensions/base_ fix._Sun Dec 4 12:51:32 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-04-12-51-32-654226000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-04-12-51-32-654226000-PST.html[jyh] Intermediate commit while considering strategy sugeessted by Aleksey._Mon Dec 5 18:40:46 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-05-18-40-46-798348000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-05-18-40-46-798348000-PST.html[jyh] Added ConsFun, containing terms of the form lambda_x. e1[x]__e2[x]__Wed Dec 7 11:22:17 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-07-11-22-17-991286000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-07-11-22-17-991286000-PST.html[jyh] Minor changes._Thu Dec 8 13:13:24 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-08-13-13-24-517903000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-08-13-13-24-517903000-PST.html[jyh] Re_investigating the list_of_fun representation._Thu Dec 8 17:01:41 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-08-17-01-41-645527000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-08-17-01-41-645527000-PST.html[jyh] This time I think I really have it solved__but we_ll see. The problem_Fri Dec 9 15:24:42 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-09-15-24-42-885918000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-09-15-24-42-885918000-PST.html[jyh] Proved the suffix part of sequent reduction._Sat Dec 10 18:46:35 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-10-18-46-35-470247000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-10-18-46-35-470247000-PST.html[jyh] Sequent reduction is finished. I don_t know if there are any_Sun Dec 11 13:48:25 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-11-13-48-25-783138000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-11-13-48-25-783138000-PST.html[jyh] Renaming files._Mon Dec 12 14:16:09 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-14-16-09-640410000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-14-16-09-640410000-PST.html[jyh] Renamed Itt_vec_sequent_term1 to Itt_vec_sequent_term._Mon Dec 12 14:23:38 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-14-23-38-536148000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-14-23-38-536148000-PST.html[jyh] Defining sequent bterms._Mon Dec 12 15:33:53 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-15-33-53-685265000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-15-33-53-685265000-PST.html[nogin] When computing dependencies, ML rules should automatically be considered_Mon Dec 12 16:30:40 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-16-30-40-497305000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-16-30-40-497305000-PST.html[nogin] Merged in the trunk changes _revisions 8123_8281___Mon Dec 12 16:50:41 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-16-50-41-302631000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-16-50-41-302631000-PST.html[jyh] Initial work on the BTerm version of sequents._Mon Dec 12 17:13:59 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-17-13-59-968146000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-17-13-59-968146000-PST.html[nogin] My lm_hash.ml change have changed the magic number._Mon Dec 12 20:10:13 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-20-10-13-152091000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-12-20-10-13-152091000-PST.html[nogin] Generated symlinks somehow got added to the repository_ removing._Tue Dec 13 15:47:59 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-13-15-47-59-163005000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-13-15-47-59-163005000-PST.html[nogin] Generated symlinks need to be ignored_Tue Dec 13 21:44:46 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-13-21-44-46-498578000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-13-21-44-46-498578000-PST.html[jyh] Some initial progress with HOAS sequent derivations._Wed Dec 14 11:50:02 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-11-50-02-904688000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-11-50-02-904688000-PST.html[nogin] Minor code clean_up. Use Lm_symbol.eq in place of _ for variables _and_Wed Dec 14 15:52:15 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-15-52-15-328218000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-15-52-15-328218000-PST.html[nogin] Improved error reporting on mismatches._Wed Dec 14 17:21:30 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-17-21-30-123958000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-17-21-30-123958000-PST.html[nogin] Ignore generated symlinks._Wed Dec 14 17:38:10 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-17-38-10-449678000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-17-38-10-449678000-PST.html[nogin] Fixing a bug _ we should not be using of_sorted_list here._Wed Dec 14 17:57:18 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-17-57-18-229505000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-17-57-18-229505000-PST.html[jyh] Another intermediate commmit._Wed Dec 14 20:44:12 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-20-44-12-819621000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-20-44-12-819621000-PST.html[kopylov] More on implementation of object theory_Wed Dec 14 22:40:40 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-22-40-40-428442000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-14-22-40-40-428442000-PST.html[kopylov] This file was commited by mistake_Thu Dec 15 12:09:33 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-15-12-09-33-916853000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-15-12-09-33-916853000-PST.html[kopylov] More on objects_Thu Dec 15 15:12:11 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-15-15-12-11-305343000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-15-15-12-11-305343000-PST.html[jyh] I was curious, so I tried the approach that Aleksey suggested._Fri Dec 16 20:05:47 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-16-20-05-47-263366000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-16-20-05-47-263366000-PST.html[nogin] Alexei _ Aleksey_ making some progress towards being able to switch to_Fri Dec 16 21:12:57 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-16-21-12-57-677274000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-16-21-12-57-677274000-PST.html[xiny] Another proof version for _reduce_vec_bind_of_mk_bterm_of_list_of_fun_ in _t2_._Sat Dec 17 23:15:25 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-17-23-15-25-365654000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-17-23-15-25-365654000-PST.html[jyh] Added enough automation to prove that _TyTop in TyExp__Sun Dec 18 15:10:14 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-18-15-10-14-940224000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-18-15-10-14-940224000-PST.html[jyh] Proved TyFun__t1_ _t2_ in TyExp._Sun Dec 18 16:56:12 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-18-16-56-12-569281000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-18-16-56-12-569281000-PST.html[jyh] Attempting the proof for TyAll__ty1_ x. _ty2[_x]_._Sun Dec 18 18:27:10 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-18-18-27-10-339351000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-18-18-27-10-339351000-PST.html[xiny] Some minor clean_ups._Mon Dec 19 00:47:04 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-00-47-04-978973000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-00-47-04-978973000-PST.html[jyh] Here is a slightly different approach, where the idea_Mon Dec 19 12:37:21 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-12-37-21-220110000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-12-37-21-220110000-PST.html[xiny] Added rewrite bind_to_list_of_fun, which I believe is needed to prove_Mon Dec 19 16:15:24 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-16-15-24-283198000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-16-15-24-283198000-PST.html[jyh] Aleksey proved the bind theorem._Mon Dec 19 17:53:01 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-17-53-01-535166000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-17-53-01-535166000-PST.html[jyh] Exploring using list_of_fun directly in Itt_hoas_bterm_wf._Mon Dec 19 18:28:44 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-18-28-44-790452000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-18-28-44-790452000-PST.html[xiny] Removed bind_to_list_of_fun._Mon Dec 19 18:36:37 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-18-36-37-938702000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-18-36-37-938702000-PST.html[jyh] Well, this is a _very_ partial approach to using list_of_fun_Mon Dec 19 20:43:07 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-20-43-07-660858000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-19-20-43-07-660858000-PST.html[nogin] _ Added a _DEFAULT_UI_ variable to the mk/config file, with possible values__Tue Dec 20 11:09:52 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-20-11-09-52-337108000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-20-11-09-52-337108000-PST.html[nogin] Made Itt_struct.nthAssumT smarter, capable of using the nth_hyp resource_Tue Dec 20 15:25:13 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-20-15-25-13-362472000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-20-15-25-13-362472000-PST.html[nogin] Further nthAssumT improvements._Tue Dec 20 20:35:16 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-20-20-35-16-536787000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-20-20-35-16-536787000-PST.html[xiny] Added foldClose2C in Itt_Struct2, and using it reproved_Wed Dec 21 00:02:27 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-00-02-27-831480000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-00-02-27-831480000-PST.html[nogin] No_op_ updating a comment_Wed Dec 21 00:42:50 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-00-42-50-854077000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-00-42-50-854077000-PST.html[nogin] Minor code simplification_Wed Dec 21 01:54:12 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-01-54-12-872504000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-01-54-12-872504000-PST.html[nogin] _ Removing the unsafe_lookup function from the Weak_memo module. We never used_Wed Dec 21 12:55:01 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-12-55-01-491972000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-12-55-01-491972000-PST.html[nogin] I believe this should finally fix the Weak_memo bug__Wed Dec 21 13:58:00 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-13-58-00-037503000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-13-58-00-037503000-PST.html[nogin] Disabling _by moving under an IFDEF_ consistency checks in Weak_memo. These_Wed Dec 21 15:46:13 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-15-46-13-168018000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-15-46-13-168018000-PST.html[nogin] Changing substT to be resource_based._Wed Dec 21 18:59:20 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-18-59-20-636866000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-18-59-20-636866000-PST.html[xiny] Added Itt_struct2.foldCloseC. The usage is_Wed Dec 21 22:35:06 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-22-35-06-675228000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-21-22-35-06-675228000-PST.html[nogin] _ Added a _sqsimple_ resource _with the term__bool output type_ that can be_Thu Dec 22 15:39:58 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-22-15-39-58-194186000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-22-15-39-58-194186000-PST.html[nogin] Added a limited support for _assert__beq_int__a__b__ to substT._Thu Dec 22 17:32:35 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-22-17-32-35-427650000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-22-17-32-35-427650000-PST.html[nogin] _ Changing the exception handling in _expand_ _ now it will no longer give up_Thu Dec 22 18:01:18 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-22-18-01-18-147731000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-22-18-01-18-147731000-PST.html[nogin] Trying to get arithT/omegaT to work better with hypotheses of the form __ _n_Thu Dec 22 20:54:10 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-22-20-54-10-750114000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-22-20-54-10-750114000-PST.html[xiny] Changed Itt_struct2.foldCloseC to use string list instead of term list._Thu Dec 22 21:16:16 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-22-21-16-16-323943000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-22-21-16-16-323943000-PST.html[xiny] Proved coalescence of bindn._Fri Dec 23 00:04:40 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-00-04-40-057886000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-00-04-40-057886000-PST.html[xiny] Added lemmas for appending two list_of_funs._Fri Dec 23 01:26:37 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-01-26-37-211590000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-01-26-37-211590000-PST.html[nogin] A number of arithT/omegaT improvements._Fri Dec 23 08:16:20 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-08-16-20-640233000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-08-16-20-640233000-PST.html[nogin] _ Proved Xin_s reduce_lof_append_lof _append of two list_of_fun_s_ lemma._Fri Dec 23 08:35:32 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-08-35-32-230311000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-08-35-32-230311000-PST.html[nogin] Further omegaT improvements._Fri Dec 23 09:56:56 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-09-56-56-072731000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-09-56-56-072731000-PST.html[nogin] This merges Itt_list2_nth with Itt_list3_nth_elem. The new operation is called_Fri Dec 23 12:40:23 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-12-40-23-190930000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-12-40-23-190930000-PST.html[nogin] Proved some of the arith lemmas_Fri Dec 23 14:04:08 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-14-04-08-709639000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-23-14-04-08-709639000-PST.html[jyh] Proved the Itt_hoas_vector.substl_substl_lof theorem._Sat Dec 24 14:53:46 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-24-14-53-46-574113000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-24-14-53-46-574113000-PST.html[jyh] I should have proved Itt_hoas_vector.append_of_substl_substl too_b_Sat Dec 24 15:02:49 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-24-15-02-49-020494000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-24-15-02-49-020494000-PST.html[xiny] Some simplifications._Sat Dec 24 17:32:42 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-24-17-32-42-470045000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-24-17-32-42-470045000-PST.html[jyh] Sorry_____Sat Dec 24 20:25:16 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-24-20-25-16-982454000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-24-20-25-16-982454000-PST.html[jyh] Proved some extra theories without the _denormalization_ theorems._Sat Dec 24 20:35:12 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-24-20-35-12-712977000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-24-20-35-12-712977000-PST.html[jyh] Removed denormalization rules from the reduce resource in Itt_hoas_vector._Sun Dec 25 17:15:57 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-25-17-15-57-640394000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-25-17-15-57-640394000-PST.html[jyh] Changed the grammar variable convention to reduce the need for quotes._Sun Dec 25 18:42:38 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-25-18-42-38-351864000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-25-18-42-38-351864000-PST.html[jyh] Membership can be stated as __term_ in _term__. I don_t know why this_Sun Dec 25 18:58:24 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-25-18-58-24-927936000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-25-18-58-24-927936000-PST.html[jyh] Adding some normalization rules for list_of_fun._Mon Dec 26 10:16:35 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-10-16-35-241321000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-10-16-35-241321000-PST.html[jyh] Separate the _sloppy_ lists from Itt_list3 into Itt_list_sloppy._Mon Dec 26 10:35:34 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-10-35-34-954750000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-10-35-34-954750000-PST.html[jyh] Working on a list_of_fun theory._Mon Dec 26 13:53:22 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-13-53-22-795265000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-13-53-22-795265000-PST.html[jyh] Added the reversible lof theory._Mon Dec 26 14:47:06 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-14-47-06-377642000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-14-47-06-377642000-PST.html[nogin] Fixing variable handling in genSOVarT._Mon Dec 26 17:45:47 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-17-45-47-265879000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-17-45-47-265879000-PST.html[jyh] Partial update to the normalizer. It doesn_t work atm, but_Mon Dec 26 18:42:43 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-18-42-43-395327000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-18-42-43-395327000-PST.html[jyh] Some progress toward normalization._Mon Dec 26 20:30:33 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-20-30-33-318331000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-20-30-33-318331000-PST.html[xiny] Small fix in foldCloseC_Mon Dec 26 21:44:23 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-21-44-23-694278000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-26-21-44-23-694278000-PST.html[nogin] In tcaT _AKA ...ttca_ and the _MustComplete_ part of autoT, give up quicker_Tue Dec 27 00:09:33 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-27-00-09-33-702800000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-27-00-09-33-702800000-PST.html[jyh] Shifted the work of normalization into the lof form,_Tue Dec 27 11:40:32 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-27-11-40-32-813825000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-27-11-40-32-813825000-PST.html[nogin] A minor autoT update._Tue Dec 27 14:14:51 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-27-14-14-51-296307000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-27-14-14-51-296307000-PST.html[jyh] Removing the second form of bind migration._Tue Dec 27 17:21:51 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-27-17-21-51-130746000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-27-17-21-51-130746000-PST.html[jyh] Added lof _rippling_ _unrelated to Bundy_s induction scheme_. The idea_Tue Dec 27 19:22:19 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-27-19-22-19-353148000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-27-19-22-19-353148000-PST.html[jyh] The _thm_ form is now supported._Wed Dec 28 11:55:39 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-28-11-55-39-029996000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-28-11-55-39-029996000-PST.html[jyh] Add initial rule boxes to reflected wf proofs._Wed Dec 28 12:06:23 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-28-12-06-23-023961000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-28-12-06-23-023961000-PST.html[jyh] Add the reflection rules to the intro resources._Wed Dec 28 12:29:15 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-28-12-29-15-527920000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-28-12-29-15-527920000-PST.html[jyh] CAUTION_ the magic number has changed_ Please save your work before_Wed Dec 28 20:11:43 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-28-20-11-43-243705000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-28-20-11-43-243705000-PST.html[xiny] Itt_hoas_lof does not need to extend Itt_hoas_bterm __ extending Itt_hoas_debruijn suffices._Thu Dec 29 13:08:16 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-29-13-08-16-176600000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-29-13-08-16-176600000-PST.html[jyh] Reformulating the Provable theorems._Thu Dec 29 13:34:16 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-29-13-34-16-533355000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-29-13-34-16-533355000-PST.html[jyh] Returning to a single logic, rather than one logic per_rule._Sat Dec 31 08:13:23 PST 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-31-08-13-23-480732000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2005-12/2005-12-31-08-13-23-480732000-PST.html