[nogin] Proved couple more induction principles _with Xin_s help_._ Mon Sep 19 06:33:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-03-613843000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-03-613843000-PDT.html [nogin] Added a quotient elimination for squiddle equality _for Yegor_._ Mon Sep 19 06:33:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-08-661791000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-08-661791000-PDT.html [yegor] mp.opt expects MP_ROOT to be set._ Mon Sep 19 06:33:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-14-625161000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-14-625161000-PDT.html [nogin] Fixed bug 327 _ added sequents supprot to TermMan.free_meta_variables._ Mon Sep 19 06:33:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-14-972551000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-14-972551000-PDT.html [yegor] Working on rewrite_based normalization of terms _polynomials_ over rationals._ Mon Sep 19 06:33:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-15-395449000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-15-395449000-PDT.html [yegor] Forgot .prla_ Mon Sep 19 06:33:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-16-036100000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-16-036100000-PDT.html [nogin] repeatC used to always do at least two identity steps in the end._ Mon Sep 19 06:33:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-17-741430000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-17-741430000-PDT.html [yegor] Replaced quotient_based definition with subset_based._ Mon Sep 19 06:33:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-18-246330000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-18-246330000-PDT.html [nogin] Sligthly nicer display from for spread._ Mon Sep 19 06:33:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-47-141562000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-47-141562000-PDT.html [nogin] Remove macropp on _omake clean__ Mon Sep 19 06:33:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-47-537205000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-47-537205000-PDT.html [nogin] Only compare the binary name from the command line with _mp.opt_/_mp.top__ Mon Sep 19 06:33:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-47-895881000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-47-895881000-PDT.html [nogin] _Bug 330_ When coming up with variable names for bound variables, it used_ Mon Sep 19 06:33:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-48-288923000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-48-288923000-PDT.html [nogin] A few updates to how contexts are handled in display forms__ Mon Sep 19 06:33:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-48-676397000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-48-676397000-PDT.html [] This commit was manufactured by cvs2svn to create branch _new_parser2_._ Mon Sep 19 06:33:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-51-669766000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-33-51-669766000-PDT.html [nogin] I_ve merged the new_parser branch with the trunk. I am putting the result_ Mon Sep 19 06:34:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-07-185934000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-07-185934000-PDT.html [nogin] In my previous commit I_ve accidentally committed the new files onto_ Mon Sep 19 06:34:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-10-918299000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-10-918299000-PDT.html [nogin] Re_adding files properly onto the new_parser2 branch._ Mon Sep 19 06:34:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-11-819109000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-11-819109000-PDT.html [nogin] _ _Bug 303_ Made sure that in shell_p4 _AKA editor/ml/mp AKA mp.run__ Mon Sep 19 06:34:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-13-303694000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-13-303694000-PDT.html [xiny] Added all basic stuff for itt_reflection, including arities of bterms_ Mon Sep 19 06:34:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-13-835029000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-13-835029000-PDT.html [nogin] Made sure theories.pdf compiles._ Mon Sep 19 06:34:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-17-144374000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-17-144374000-PDT.html [nogin] The tests that require ITT should not be compiled unless ITT is listed in_ Mon Sep 19 06:34:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-18-323046000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-18-323046000-PDT.html [nogin] Fixing a typo in my previous commit._ Mon Sep 19 06:34:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-18-724115000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-18-724115000-PDT.html [nogin] Made sure CIC compiles._ Mon Sep 19 06:34:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-19-093594000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-19-093594000-PDT.html [yegor] 1. Addressing the bug 322 _first part about nat__ Mon Sep 19 06:34:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-19-684637000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-19-684637000-PDT.html [yegor] itt_int_arith _ fixing a bug discovered while doing normalization for rationals_ Mon Sep 19 06:34:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-43-154299000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-43-154299000-PDT.html [yegor] Forgot to commit yesterday_ Mon Sep 19 06:34:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-43-643541000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-43-643541000-PDT.html [yegor] Forgot to remove temporary debug code. Sorry._ Mon Sep 19 06:34:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-44-097682000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-44-097682000-PDT.html [nogin] A bit of standartization of debug variables__ Mon Sep 19 06:34:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-44-519658000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-44-519658000-PDT.html [nogin] _Bug 322_ Itt_nat.nat2ge should not change the type from nat to int._ Mon Sep 19 06:34:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-45-571833000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-45-571833000-PDT.html [yegor] With this fix arithT does not fail on /itt_nat/natFullInduction/1/1/1 even without_ Mon Sep 19 06:34:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-48-754276000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-48-754276000-PDT.html [yegor] 1.Added _nat__n_ in hyps_ to ge_elim resource for Arith._ Mon Sep 19 06:34:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-49-162928000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-49-162928000-PDT.html [yegor] Fixes for proofs broken by a change in Itt_nat.indEquality made yesterday._ Mon Sep 19 06:34:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-50-832654000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-10/2005-09-19-06-34-50-832654000-PDT.html