[jyh] Rephrased the Provable intro rules, using the SubLogic judgment_Sun Jan 1 09:15:25 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-01-09-15-25-130689000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-01-09-15-25-130689000-PST.html[jyh] Added initial Provability tactic._Sun Jan 1 12:56:27 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-01-12-56-27-276559000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-01-12-56-27-276559000-PST.html[jyh] Added Itt_list_set for new set_style theorems about lists._Sun Jan 1 13:53:37 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-01-13-53-37-478540000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-01-13-53-37-478540000-PST.html[jyh] Added less ambiguous names for some of the refiner functions _for names_Mon Jan 2 11:27:13 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-02-11-27-13-402877000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-02-11-27-13-402877000-PST.html[jyh] Added vector binders to the BTerm normalizer._Mon Jan 2 16:23:16 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-02-16-23-16-297852000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-02-16-23-16-297852000-PST.html[jyh] Rename Meta_extensions_theory to Meta_context_theory._Mon Jan 2 16:27:31 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-02-16-27-31-144237000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-02-16-27-31-144237000-PST.html[jyh] Still working on well_formedness of reflected vector terms._Mon Jan 2 17:32:15 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-02-17-32-15-809451000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-02-17-32-15-809451000-PST.html[jyh] Added a simple forward_chaining tactic in support/tactics/forward.ml_Tue Jan 3 13:05:54 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-03-13-05-54-366933000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-03-13-05-54-366933000-PST.html[jyh] Changed the proof witness code in Itt_hoas_sequent_proof from_Wed Jan 4 08:30:08 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-04-08-30-08-786801000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-04-08-30-08-786801000-PST.html[xiny] Completed proofs in Itt_hoas_bterm_wf. However, I added a well_formedness_Wed Jan 4 17:26:52 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-04-17-26-52-331238000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-04-17-26-52-331238000-PST.html[xiny] Now really proved theorems in Itt_hoas_bterm_wf, with useless well_formedness subgoals removed._Wed Jan 4 17:51:17 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-04-17-51-17-666114000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-04-17-51-17-666114000-PST.html[nogin] Include the SVN revision number _when available_ in the MetaPRL version string._Thu Jan 5 13:16:42 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-05-13-16-42-867232000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-05-13-16-42-867232000-PST.html[nogin] _ Minor clean_up of the debugging code._Thu Jan 5 17:18:53 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-05-17-18-53-760512000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-05-17-18-53-760512000-PST.html[jyh] Re_added the Itt_hoas_sequent.bterm2_is_bterm rule. However, this is_Thu Jan 5 20:29:47 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-05-20-29-47-821098000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-05-20-29-47-821098000-PST.html[nogin] _Issue 560_ Give a better error message when a theory does not exist._Thu Jan 5 22:36:38 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-05-22-36-38-614757000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-05-22-36-38-614757000-PST.html[nogin] _Issue 561_ The format of editor/ml/mldebug.dir is different on Windows._Thu Jan 5 22:42:30 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-05-22-42-30-578446000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-05-22-42-30-578446000-PST.html[jyh] Updated the incomplete proofs._Fri Jan 6 08:43:09 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-08-43-09-806067000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-08-43-09-806067000-PST.html[nogin] Incrementing the version numbers for the ASCII and binary formats to account_Fri Jan 6 10:50:37 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-10-50-37-979214000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-10-50-37-979214000-PST.html[nogin] Spelling fixes_Fri Jan 6 14:14:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-14-14-29-484350000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-14-14-29-484350000-PST.html[nogin] Revision_based status checking._Fri Jan 6 15:40:11 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-15-40-11-273794000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-15-40-11-273794000-PST.html[yegor] Fixed the problem noticed by Aleksey _ one_only_constraint case was treated incorrectly_Fri Jan 6 17:55:12 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-17-55-12-899651000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-17-55-12-899651000-PST.html[nogin] _ Itt_nat should extend Itt_omega_Fri Jan 6 21:31:33 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-21-31-33-322351000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-21-31-33-322351000-PST.html[nogin] _ Updated arithT to generate fewer wf subgoals._Fri Jan 6 22:16:34 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-22-16-34-995705000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-22-16-34-995705000-PST.html[nogin] Minor omegaT optimization._Fri Jan 6 23:27:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-23-27-01-086587000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-06-23-27-01-086587000-PST.html[nogin] Another minor omegaT optimization _that should reduce the number of wf_Sat Jan 7 00:07:36 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-07-00-07-37-004122000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-07-00-07-37-004122000-PST.html[nogin] Making _omake clean_ more clean._Sat Jan 7 09:14:18 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-07-09-14-18-934631000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-07-09-14-18-934631000-PST.html[jyh] Simplfy the BTerm normalizer a bit. This now uses a single_Sat Jan 7 10:43:34 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-07-10-43-34-400883000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-07-10-43-34-400883000-PST.html[nogin] Adding poplmark/naive to the _THEORIES_all_ list._Sat Jan 7 11:36:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-07-11-36-29-277320000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-07-11-36-29-277320000-PST.html[nogin] In proof browsing UI __down 0__, give more information about the rewrites._Sat Jan 7 13:36:46 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-07-13-36-46-951204000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-07-13-36-46-951204000-PST.html[jyh] Updated the forward_chainer to use a more efficient algorithm _bug _562_._Sun Jan 8 12:51:14 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-08-12-51-14-716604000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-08-12-51-14-716604000-PST.html[nogin] Added sqsimple_BTerm__n__ to sqsimple resource_Sun Jan 8 15:57:11 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-08-15-57-11-450822000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-08-15-57-11-450822000-PST.html[jyh] Ok, enough for now. The basic rules in Pmn_core_terms are proved._Sun Jan 8 21:01:40 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-08-21-01-40-492080000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-08-21-01-40-492080000-PST.html[jyh] Experimenting with optimization._Mon Jan 9 12:51:03 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-09-12-51-03-505731000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-09-12-51-03-505731000-PST.html[jyh] Investigate a new plan of attack, where we prove theorems for all the_Mon Jan 9 14:20:15 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-09-14-20-15-478420000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-09-14-20-15-478420000-PST.html[jyh] Proved the initial set of simple theorems._Mon Jan 9 14:30:20 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-09-14-30-20-333021000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-09-14-30-20-333021000-PST.html[jyh] Added the _simple_ BTerm normalizer. This didn_t work as well_Mon Jan 9 19:24:24 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-09-19-24-24-748952000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-09-19-24-24-748952000-PST.html[nogin] Teaching autoT that _1 _ 2 in nat_ and _1 _ 2 in int_ are contradictory_Mon Jan 9 20:13:59 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-09-20-13-59-899368000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-09-20-13-59-899368000-PST.html[nogin] Memory usage optimization in prefix_thenLocalLabelT_Tue Jan 10 05:47:02 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-05-47-02-222735000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-05-47-02-222735000-PST.html[nogin] Minor reduceT optimization._Tue Jan 10 12:35:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-12-35-01-277229000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-12-35-01-277229000-PST.html[nogin] Small arithT optimization._Tue Jan 10 13:05:15 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-13-05-15-500095000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-13-05-15-500095000-PST.html[jyh] Minor changes as I try to understand the problem with label_Tue Jan 10 13:27:52 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-13-27-52-119762000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-13-27-52-119762000-PST.html[nogin] reduceC for __ and __ optimization__Tue Jan 10 14:42:54 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-14-42-54-878352000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-14-42-54-878352000-PST.html[nogin] The poplmark/naive theory was missing a _clean_ target._Tue Jan 10 14:46:17 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-14-46-17-714182000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-14-46-17-714182000-PST.html[jyh] Check whether forward_chaining ever produces more than one _main_ subgoal._Tue Jan 10 15:09:19 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-15-09-19-102685000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-15-09-19-102685000-PST.html[jyh] Minor adjustment fixes the problem with forward_chaining__Tue Jan 10 15:26:04 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-15-26-04-280585000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-15-26-04-280585000-PST.html[jyh] Oops, actually I did break the proofs with a bogus addrC._Tue Jan 10 15:30:55 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-15-30-55-451666000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-15-30-55-451666000-PST.html[jyh] Added the four expressions _of type Exp_._Tue Jan 10 16:47:37 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-16-47-37-130069000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-16-47-37-130069000-PST.html[jyh] Added all syntax except the fsub sequent._Tue Jan 10 16:59:49 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-16-59-49-337094000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-10-16-59-49-337094000-PST.html[nogin] _ Use the location information _that is now available thanks to Jason_s rev_Wed Jan 11 00:48:44 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-11-00-48-44-429349000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-11-00-48-44-429349000-PST.html[nogin] Reduce annotations on conditional rewrites ___ for all the 0_arity SO_Wed Jan 11 09:22:33 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-11-09-22-33-547181000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-11-09-22-33-547181000-PST.html[nogin] Modifying a bit the reduce annotation approach that I_ve added in the previous_Wed Jan 11 13:32:27 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-11-13-32-27-760239000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-11-13-32-27-760239000-PST.html[jyh] Add a conversion from sequents to BTerms._Wed Jan 11 19:41:33 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-11-19-41-33-887709000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-11-19-41-33-887709000-PST.html[jyh] Reproved all the theorems in Itt_hoas_proof1 without _ty_sequent_Thu Jan 12 15:46:40 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-12-15-46-40-161304000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-12-15-46-40-161304000-PST.html[jyh] Forgot to commit the proofs._Thu Jan 12 15:52:20 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-12-15-52-20-164844000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-12-15-52-20-164844000-PST.html[nogin] Added an intro annotation on a rule._Thu Jan 12 17:38:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-12-17-38-29-936178000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-12-17-38-29-936178000-PST.html[nogin] The Itt_hoas_util.elim_bdepth rule __OmegaT is failing on some artihmetic, so_Thu Jan 12 18:04:03 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-12-18-04-03-997906000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-12-18-04-03-997906000-PST.html[jyh] Working on the inverse function that transforms a BTerm back into_Thu Jan 12 20:15:07 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-12-20-15-07-747530000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-12-20-15-07-747530000-PST.html[jyh] Added the sequent_of_bterm__e_ that converts back from a BTerm_Fri Jan 13 12:09:25 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-12-09-25-175107000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-12-09-25-175107000-PST.html[jyh] Convert sequents to BTerms._Fri Jan 13 12:26:09 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-12-26-09-263521000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-12-26-09-263521000-PST.html[jyh] Working on proof steps._Fri Jan 13 13:04:04 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-13-04-04-731445000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-13-04-04-731445000-PST.html[jyh] Further cleanup wrt BTerm sequents._Fri Jan 13 14:37:07 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-14-37-07-860184000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-14-37-07-860184000-PST.html[nogin] _ Do pro_active normalization of the numerical expressions _so that they are_Fri Jan 13 14:42:13 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-14-42-13-188145000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-14-42-13-188145000-PST.html[nogin] Rippling is no longer needed__Fri Jan 13 15:28:40 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-15-28-40-855920000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-15-28-40-855920000-PST.html[nogin] _ Filter_ when copying proofs from an old .prla/.prlb/.cmoz, pick up any_Fri Jan 13 18:53:18 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-18-53-18-788136000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-18-53-18-788136000-PST.html[nogin] Minor optimization_ use _n_0_ instead of _not_n_0 in nat__ in conditional_Fri Jan 13 19:05:48 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-19-05-48-153983000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-19-05-48-153983000-PST.html[nogin] Now that the arithmetical reduction is in place, the lof_nil lists will always_Fri Jan 13 20:10:31 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-20-10-31-117490000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-13-20-10-31-117490000-PST.html[xiny] Proved the _provable_elim_ theorem._Sat Jan 14 00:52:31 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-00-52-31-771640000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-00-52-31-771640000-PST.html[jyh] I think we do not need the type BSequent for the bterms that represent_Sat Jan 14 08:20:46 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-08-20-46-021795000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-08-20-46-021795000-PST.html[jyh] Allow bindings in the forward rules in Itt_hoas_bterm_wf._Sat Jan 14 09:06:13 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-09-06-13-811340000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-09-06-13-811340000-PST.html[nogin] Trying to optimize onSomeHypT _autoT_s version of onSomeHypT nthHypT_._Sat Jan 14 13:07:36 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-13-07-36-572242000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-13-07-36-572242000-PST.html[nogin] _ Added to nth_hyp_ _t in BTerm__d_ ___ _d _ bdepth__t_ in int_Sat Jan 14 15:20:07 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-15-20-07-978870000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-15-20-07-978870000-PST.html[jyh] Well, after much work, I_ll probably need to take another approach_Sat Jan 14 17:07:30 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-17-07-30-478378000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-17-07-30-478378000-PST.html[nogin] The dest_bterm_mk_term2 rewrite in Itt_hoas_bterm had wf conditions that were_Sat Jan 14 19:22:33 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-19-22-33-367871000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-19-22-33-367871000-PST.html[jyh] Working on relaxed wf constraints._Sat Jan 14 20:00:23 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-20-00-23-237410000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-20-00-23-237410000-PST.html[nogin] Merged in the trunk changes _revisions 8281_8481___Sat Jan 14 21:13:11 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-21-13-11-595571000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-14-21-13-11-595571000-PST.html[xiny] Added elimination rules which do not do thinning. The one with bindings is hard_ not proved yet._Sun Jan 15 01:14:10 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-15-01-14-10-496854000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-15-01-14-10-496854000-PST.html[jyh] Proved the relaxed eta_reduction rules._Sun Jan 15 13:09:21 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-15-13-09-21-010259000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-15-13-09-21-010259000-PST.html[nogin] Proved eta_reduction under mk_bterm._Sun Jan 15 16:12:28 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-15-16-12-28-129094000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-15-16-12-28-129094000-PST.html[jyh] Basic relaxed theory._Sun Jan 15 17:47:21 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-15-17-47-21-784465000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-15-17-47-21-784465000-PST.html[jyh] Reproved the Itt_hoas_sequent_bterm1 using relaxed properties._Sun Jan 15 21:29:42 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-15-21-29-42-173688000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-15-21-29-42-173688000-PST.html[jyh] NOTE_ this is a moderate change to the internal way we handle_Mon Jan 16 20:13:52 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-16-20-13-52-945585000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-16-20-13-52-945585000-PST.html[jyh] Define super_relaxed rewrites. I forgot that bsequent__ ... ___Mon Jan 16 21:53:31 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-16-21-53-31-594863000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-16-21-53-31-594863000-PST.html[jyh] Added the _select option to wrap_reduce._Tue Jan 17 00:49:23 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-00-49-23-453120000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-00-49-23-453120000-PST.html[jyh] For reduce, the _select argument should be a string list._Tue Jan 17 08:52:37 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-08-52-37-184128000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-08-52-37-184128000-PST.html[jyh] Proved the relaxed reduction rules._Tue Jan 17 09:02:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-09-02-29-639424000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-09-02-29-639424000-PST.html[jyh] Changes to options__Tue Jan 17 13:39:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-13-39-29-633246000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-13-39-29-633246000-PST.html[jyh] Further changes _this is all I plan to do for the moment_._Tue Jan 17 14:45:50 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-14-45-50-164258000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-14-45-50-164258000-PST.html[jyh] Roll back the changes to Mp_resource. Clearly I don_t know what I am_Tue Jan 17 15:35:56 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-15-35-56-486779000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-15-35-56-486779000-PST.html[jyh] Forgot to commit option_sig.ml._Tue Jan 17 16:10:56 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-16-10-56-679991000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-16-10-56-679991000-PST.html[jyh] Allow preprocessing on the tactic_arg before the proof is created._Tue Jan 17 16:53:53 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-16-53-53-010174000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-16-53-53-010174000-PST.html[xiny] Finally proved the elimination rule thanks to Aleksey_ my original statement was wrong._Tue Jan 17 17:28:32 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-17-28-32-207438000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-17-28-32-207438000-PST.html[xiny] Cleaned the theory._Tue Jan 17 17:49:19 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-17-49-19-421751000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-17-49-19-421751000-PST.html[nogin] Minor_ eagerly compose the functions._Tue Jan 17 18:28:45 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-18-28-45-248972000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-18-28-45-248972000-PST.html[jyh] Reproving theorems in Itt_hoas_sequent_bterm2._Tue Jan 17 20:53:09 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-20-53-09-634365000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-20-53-09-634365000-PST.html[nogin] ___ WARNING _ BREAKS BINARY COMPATIBILITY ____Tue Jan 17 23:44:11 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-23-44-11-717761000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-17-23-44-11-717761000-PST.html[jyh] Implemented Aleksey_s scheme for options._Wed Jan 18 11:11:37 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-18-11-11-37-459034000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-18-11-11-37-459034000-PST.html[jyh] Fixed a bug with OptionIgnore _it was getting ignored_._Wed Jan 18 11:21:35 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-18-11-21-35-186983000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-18-11-21-35-186983000-PST.html[nogin] Small reduceC/reduceT optimization._Wed Jan 18 16:35:20 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-18-16-35-20-324775000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-18-16-35-20-324775000-PST.html[jyh] Prepare an installable version of MetaPRL._Wed Jan 18 20:14:02 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-18-20-14-02-482539000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-18-20-14-02-482539000-PST.html[jyh] Prepare an installable version of MetaPRL._Wed Jan 18 20:14:02 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-18-20-14-02-482539000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-18-20-14-02-482539000-PST.html[nogin] Internalized the handling of allSubC_Wed Jan 18 23:25:44 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-18-23-25-44-675721000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-18-23-25-44-675721000-PST.html[nogin] Use termC instead of funC, where appropriate._Thu Jan 19 01:21:40 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-01-21-40-105289000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-01-21-40-105289000-PST.html[nogin] Rewrote the rewrite_boot engine a bit, trying to make things like higherC_Thu Jan 19 02:07:10 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-02-07-10-714589000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-02-07-10-714589000-PST.html[nogin] Do not run JProver when there are no logical formulas anywhere in the_Thu Jan 19 03:23:47 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-03-23-47-765369000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-03-23-47-765369000-PST.html[nogin] Removed a redundant tactic from autoT._Thu Jan 19 06:32:37 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-06-32-37-790482000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-06-32-37-790482000-PST.html[jyh] Reconfigure MetaPRL to allow an installable version._Thu Jan 19 14:03:10 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-14-03-10-137904000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-14-03-10-137904000-PST.html[nogin] Cleaning up things after Jason_s big _shared r/o installation_ commit,_Thu Jan 19 17:39:10 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-17-39-10-096347000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-17-39-10-096347000-PST.html[jyh] _Every_ theory will install itself._Thu Jan 19 18:16:16 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-18-16-16-557207000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-18-16-16-557207000-PST.html[nogin] For now _until a new OMake is released_, include the /dummy_scanner_Thu Jan 19 18:32:20 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-18-32-20-279651000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-18-32-20-279651000-PST.html[nogin] Itt_logic_ filter out the _irrelevant_ hyps/assums before running JProver._Thu Jan 19 18:51:30 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-18-51-30-941489000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-18-51-30-941489000-PST.html[nogin] Make sure the _linkall is used in all the right places._Thu Jan 19 18:52:24 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-18-52-24-770014000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-18-52-24-770014000-PST.html[jyh] Separate the theory configuration from the build specification._Thu Jan 19 19:22:58 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-19-22-58-254076000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-19-22-58-254076000-PST.html[nogin] Minor cleanup._Thu Jan 19 19:28:46 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-19-28-46-149058000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-19-28-46-149058000-PST.html[nogin] Adding a _clean_ target to the default theory body._Thu Jan 19 19:43:59 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-19-43-59-797632000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-19-43-59-797632000-PST.html[jyh] Added the INSTALL_DIR option to mk/config, and generate_Thu Jan 19 20:36:14 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-20-36-14-103988000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-20-36-14-103988000-PST.html[jyh] Add a THEORYPATH search path for theories._Thu Jan 19 20:59:27 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-20-59-27-147904000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-20-59-27-147904000-PST.html[nogin] Made it possible to actually change the THEORY_PATH variable._Thu Jan 19 21:34:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-21-34-29-307758000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-21-34-29-307758000-PST.html[jyh] OCAMLINCLUDES[] was computed incorrectly in the Theory_files_ function._Thu Jan 19 21:43:02 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-21-43-02-373474000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-21-43-02-373474000-PST.html[jyh] Yay_ The standalone MetaPRL brings up the browser._Thu Jan 19 22:31:54 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-22-31-54-823000000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-22-31-54-823000000-PST.html[jyh] At this point, I_m just tweaking the config._Thu Jan 19 23:27:34 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-23-27-34-158055000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-23-27-34-158055000-PST.html[jyh] Hmm, I seem to have broke the compilation because I named it_Thu Jan 19 23:29:52 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-23-29-52-791330000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-19-23-29-52-791330000-PST.html[nogin] Do not install the .prla_Fri Jan 20 00:19:39 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-00-19-39-926584000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-00-19-39-926584000-PST.html[nogin] Fixed a bug in the context teleportation axiom for cases where the context_Fri Jan 20 04:45:47 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-04-45-47-232403000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-04-45-47-232403000-PST.html[nogin] Fixed bytecode compilation _including mp.run__Fri Jan 20 13:38:31 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-13-38-31-062138000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-13-38-31-062138000-PST.html[nogin] Proved 0 ____ 1, thus demonstrating that_Fri Jan 20 15:49:16 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-15-49-16-256417000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-15-49-16-256417000-PST.html[nogin] Fixing a display form typo._Fri Jan 20 16:37:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-16-37-01-759186000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-16-37-01-759186000-PST.html[nogin] Made the reduce_sequent_ind_base1 rewrite more conservative._Fri Jan 20 17:00:47 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-17-00-47-126728000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-17-00-47-126728000-PST.html[nogin] _ MetaPRL is compatible with OCaml 3.09.1_Fri Jan 20 18:58:39 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-18-58-39-745947000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-18-58-39-745947000-PST.html[jyh] The new patch for check OCaml versions was breaking because_Fri Jan 20 20:59:19 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-20-59-19-033046000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-20-20-59-19-033046000-PST.html[jyh] Move the MetaPRL scripts from editor/ml into support/editor_Sat Jan 21 07:45:49 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-07-45-49-077799000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-07-45-49-077799000-PST.html[jyh] Temporarily, at least, link the mpopt script into editor/ml_Sat Jan 21 08:18:03 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-08-18-03-637064000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-08-18-03-637064000-PST.html[nogin] Keep all the scripts in support/editor. All the scripts that are postentially_Sat Jan 21 16:37:25 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-16-37-25-547424000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-16-37-25-547424000-PST.html[jyh] Some changes for the OCaml book._Sat Jan 21 18:08:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-18-08-29-987448000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-18-08-29-987448000-PST.html[jyh] Add initial jyh repository._Sat Jan 21 18:34:58 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-18-34-58-019827000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-18-34-58-019827000-PST.html[jyh] The _____ in the mk/config message is now ____Sat Jan 21 19:08:09 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-19-08-09-546028000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-19-08-09-546028000-PST.html[jyh] As usual, svn does not recognize svn_externals until you commit._Sat Jan 21 19:35:00 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-19-35-00-964322000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-19-35-00-964322000-PST.html[jyh] In the theory search _OMakefile_theories.find_theory_, do not_Sat Jan 21 19:48:12 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-19-48-12-568682000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-19-48-12-568682000-PST.html[jyh] Initial jyh theory._Sat Jan 21 20:02:22 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-20-02-22-496081000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-20-02-22-496081000-PST.html[nogin] The new symlinks should be ignored by SVN and deleted by _omake clean_._Sat Jan 21 22:52:23 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-22-52-23-019180000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-21-22-52-23-019180000-PST.html[jyh] Include the theory in the theory search path even if it is READONLY._Sun Jan 22 11:35:39 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-22-11-35-39-568310000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-22-11-35-39-568310000-PST.html[jyh] Added intro and elim rules for BindTriangle_n_._Sun Jan 22 16:28:13 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-22-16-28-13-715251000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-22-16-28-13-715251000-PST.html[jyh] [Ping Aleksey] Take a look at the following address__Sun Jan 22 21:17:12 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-22-21-17-12-715225000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-22-21-17-12-715225000-PST.html[jyh] Power failure her, comitting before everything dies._Mon Jan 23 00:34:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-00-34-01-555497000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-00-34-01-555497000-PST.html[jyh] Reverted the change that moved itt/reflection out of the itt/_Mon Jan 23 14:33:12 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-14-33-12-884574000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-14-33-12-884574000-PST.html[nogin] _ MetaPRL _especially the read_only mode_ requires OMake 0.9.6.8_Mon Jan 23 14:47:41 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-14-47-41-964730000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-14-47-41-964730000-PST.html[jyh] Added some theorems about nil and singleton lists in the Itt_vec_sequent_term_Mon Jan 23 18:39:51 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-18-39-51-130281000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-18-39-51-130281000-PST.html[nogin] Made the default browser command configurable via the mk/config._Mon Jan 23 18:42:14 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-18-42-14-926482000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-18-42-14-926482000-PST.html[nogin] TUrned a prim_rw into a define._Mon Jan 23 19:22:41 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-19-22-41-262525000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-19-22-41-262525000-PST.html[nogin] In the readonly installation mode, we currently do not have doc/htmlman _ so_Mon Jan 23 19:59:18 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-19-59-18-967213000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-19-59-18-967213000-PST.html[nogin] Fixing a non_compile, sorry__Mon Jan 23 20:06:20 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-20-06-20-747780000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-20-06-20-747780000-PST.html[jyh] Include .test_metaprl_startup on _omake install_._Mon Jan 23 20:36:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-20-36-01-107993000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-20-36-01-107993000-PST.html[nogin] _ When no port is given _or when _port 0 is given_, use the first free port_Mon Jan 23 20:51:25 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-20-51-25-698743000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-20-51-25-698743000-PST.html[jyh] Xin_ I plan to merge the _branch_ tomorrow, renaming all the numbered_Mon Jan 23 21:12:19 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-21-12-19-283169000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-21-12-19-283169000-PST.html[nogin] Fixed the DEFAUILT_UI detection._Mon Jan 23 21:32:40 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-21-32-40-561722000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-23-21-32-40-561722000-PST.html[jyh] I can_t rename files atomically, so this is the first step__Tue Jan 24 09:59:47 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-09-59-47-169329000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-09-59-47-169329000-PST.html[jyh] Comment out Pmn_core_terms temporarily._Tue Jan 24 10:51:04 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-10-51-04-151305000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-10-51-04-151305000-PST.html[jyh] Renamed numbered files back to unnumbered._Tue Jan 24 10:51:52 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-10-51-52-410223000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-10-51-52-410223000-PST.html[jyh] Fix Filter_reflection to use the new terms and_Tue Jan 24 11:08:16 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-11-08-17-002202000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-11-08-17-002202000-PST.html[jyh] Added with withOptionC and withoutOptionC conversions._Tue Jan 24 11:54:36 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-11-54-36-975016000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-11-54-36-975016000-PST.html[nogin] _ Making the _omake clean_ more clean, while making sure that in shared mode,_Tue Jan 24 13:28:30 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-13-28-30-735074000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-13-28-30-735074000-PST.html[nogin] Making _omake clean_ more clean._Tue Jan 24 13:33:37 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-13-33-37-083551000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-13-33-37-083551000-PST.html[nogin] Making _omake clean_ more clean._Tue Jan 24 13:33:37 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-13-33-37-083551000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-13-33-37-083551000-PST.html[jyh] Also initialize the tactic_arg in proofs loaded from IO proofs._Tue Jan 24 13:34:07 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-13-34-07-484389000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-13-34-07-484389000-PST.html[nogin] _ Better scoping of build options._Tue Jan 24 14:38:38 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-14-38-38-130885000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-14-38-38-130885000-PST.html[jyh] Try to be more careful about using length_vlist__ _J_ ___ as_Tue Jan 24 15:08:11 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-15-08-11-175063000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-15-08-11-175063000-PST.html[jyh] We_re back in business in PoplMark, at least for the first three_Tue Jan 24 18:23:01 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-18-23-01-691430000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-18-23-01-691430000-PST.html[jyh] Fixed a couple of broken theorems._Tue Jan 24 18:41:05 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-18-41-05-331890000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-18-41-05-331890000-PST.html[jyh] Split the judgments out of Pmn_core_terms._Tue Jan 24 19:40:54 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-19-40-54-547298000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-19-40-54-547298000-PST.html[jyh] Split the judgments out of Pmn_core_terms._Tue Jan 24 19:40:54 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-19-40-54-547298000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-24-19-40-54-547298000-PST.html[jyh] Reflected rule definitions can use the usual meta_type checking_Wed Jan 25 09:57:49 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-25-09-57-49-793704000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-25-09-57-49-793704000-PST.html[nogin] Remove the __EXPORT_ directory on _omake clean_._Wed Jan 25 19:16:15 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-25-19-16-15-027818000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-25-19-16-15-027818000-PST.html[nogin] Fixing the svnversion test._Wed Jan 25 20:28:49 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-25-20-28-49-462018000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-25-20-28-49-462018000-PST.html[nogin] Compute the version string manually when svnversion does not exist, but_Wed Jan 25 20:58:53 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-25-20-58-53-178744000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-25-20-58-53-178744000-PST.html[nogin] Better svnversion replacement._Wed Jan 25 23:02:35 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-25-23-02-35-204738000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-25-23-02-35-204738000-PST.html[nogin] Truncate the _id_ number to 31 bits in order to make .prla files written on_Thu Jan 26 00:09:59 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-26-00-09-59-626589000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-26-00-09-59-626589000-PST.html[nogin] I do not think we need to run check_status.sh from under ssh anymore._Thu Jan 26 00:17:29 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-26-00-17-29-722404000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-26-00-17-29-722404000-PST.html[nogin] _ Make sure that selection options in tactic_arg do not pollute the _named_Thu Jan 26 00:28:26 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-26-00-28-26-188978000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-26-00-28-26-188978000-PST.html[nogin] ___ WARNING_ BREAKS BINARY COMPATIBILITY_ ____Thu Jan 26 00:50:57 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-26-00-50-57-423002000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-26-00-50-57-423002000-PST.html[nogin] Adding a meta_type for selection opnames._Thu Jan 26 18:57:39 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-26-18-57-40-004178000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-26-18-57-40-004178000-PST.html[jyh] Partial progress to computing the elimination rule._Thu Jan 26 21:30:59 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-26-21-30-59-572284000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-26-21-30-59-572284000-PST.html[jyh] Generate the elim_rule. It is both big and ugly._Fri Jan 27 10:28:22 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-27-10-28-22-978448000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-27-10-28-22-978448000-PST.html[nogin] Fixed a typo._Fri Jan 27 14:20:03 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-27-14-20-03-243034000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-27-14-20-03-243034000-PST.html[nogin] Moving the settings of the OMake variables to mk/default. This way, mk/config_Fri Jan 27 14:25:15 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-27-14-25-15-329565000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-27-14-25-15-329565000-PST.html[jyh] Manually branch the reflection/experimental directory_Sat Jan 28 18:59:39 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-28-18-59-39-265963000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-28-18-59-39-265963000-PST.html[jyh] Added append vector binders and proved some really basic theorems._Sat Jan 28 19:54:47 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-28-19-54-47-112659000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-28-19-54-47-112659000-PST.html[jyh] Initial progress toward append_style sequents and binders._Sun Jan 29 17:41:43 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-29-17-41-43-298073000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-29-17-41-43-298073000-PST.html[yegor] Committing changes made back in Decmeber before my defense._Sun Jan 29 18:46:26 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-29-18-46-26-423918000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-29-18-46-26-423918000-PST.html[jyh] Added a _squashed_ version of sequent induction. It can be removed_Sun Jan 29 19:20:47 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-29-19-20-47-535823000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-29-19-20-47-535823000-PST.html[yegor] unintentionally, I deleted all the new proofs, so I had to restore them, luckily they are trivial._Sun Jan 29 20:48:31 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-29-20-48-31-466072000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-01/2006-01-29-20-48-31-466072000-PST.html