[steph] ___ empty log message ____ Mon Sep 19 02:19:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-18-195532000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-18-195532000-PDT.html [nogin] Updated the CVS documentation URL._ Mon Sep 19 02:19:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-19-879586000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-19-879586000-PDT.html [nogin] Enabled the _strict_ rewriter mode._ Mon Sep 19 02:19:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-20-244041000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-20-244041000-PDT.html [nogin] Now z.ml runs again_ Mon Sep 19 02:19:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-21-232227000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-21-232227000-PDT.html [nogin] Fixed the jtest function_ Mon Sep 19 02:19:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-21-587487000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-21-587487000-PDT.html [nogin] Now __cd _/theory___ also initializes the theory, so there is no need_ Mon Sep 19 02:19:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-21-945665000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-21-945665000-PDT.html [nogin] Some .mlz files were not marked as such in Makefiles _ fixed_ Mon Sep 19 02:19:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-22-362439000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-22-362439000-PDT.html [nogin] Moved all the test files to the tests directory to keep things cleaner_ Mon Sep 19 02:19:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-22-785614000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-22-785614000-PDT.html [nogin] _ When compiling a MetaPRL file referenced using its path instead of_ Mon Sep 19 02:19:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-23-927642000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-23-927642000-PDT.html [nogin] Restored the old code for proving the propositional pigeon_hole principle._ Mon Sep 19 02:19:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-26-070829000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-26-070829000-PDT.html [nogin] Renamed_ Mon Sep 19 02:19:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-26-727983000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-26-727983000-PDT.html [nogin] These are obsolete._ Mon Sep 19 02:19:27 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-27-215587000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-27-215587000-PDT.html [nogin] Fixed the _profile_ target in the Makefile. I still have to fix my Ocaml_ Mon Sep 19 02:19:27 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-27-645843000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-27-645843000-PDT.html [nogin] Prefixed the Failure messages with the module name._ Mon Sep 19 02:19:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-28-015914000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-28-015914000-PDT.html [nogin] Fixed a bug in the _Strict_ rewriter mode._ Mon Sep 19 02:19:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-28-541753000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-28-541753000-PDT.html [nogin] ._ Mon Sep 19 02:19:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-28-954550000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-28-954550000-PDT.html [krupski] tptp_prove1.ml_ is a copy of tptp_prove.ml_ with old unification replaced_ Mon Sep 19 02:19:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-29-280058000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-29-280058000-PDT.html [krupski] I switch off the error messages produced by old unification._ Mon Sep 19 02:19:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-30-049763000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-30-049763000-PDT.html [nogin] _ Fixed the prop_pigeon tactics._ Mon Sep 19 02:19:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-30-420164000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-30-420164000-PDT.html [nogin] When a list of subgoals is too big, displaying used to take a while. I implemented a_ Mon Sep 19 02:19:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-30-952489000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-30-952489000-PDT.html [nogin] Added profiling comtrol to some tests_ Mon Sep 19 02:19:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-31-382307000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-31-382307000-PDT.html [nogin] Small bugfixes_ Mon Sep 19 02:19:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-32-486970000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-32-486970000-PDT.html [nogin] _ The strict rewriter mode allowed me to replace the ml_rule thin with an ordinary_ Mon Sep 19 02:19:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-32-851169000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-32-851169000-PDT.html [nogin] When building contractum we used to build a new operator each time we wanted_ Mon Sep 19 02:19:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-33-305345000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-33-305345000-PDT.html [nogin] Added a new function for free variable testing._ Mon Sep 19 02:19:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-33-962584000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-33-962584000-PDT.html [jyh] Itt_bool now expands._ Mon Sep 19 02:19:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-34-627751000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-19-34-627751000-PDT.html [nogin] Fixed the ASCII files generation to correctly handle the situation_ Mon Sep 19 02:23:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-23-52-778838000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-23-52-778838000-PDT.html [nogin] Efficiency fixes._ Mon Sep 19 02:23:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-23-53-420653000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-23-53-420653000-PDT.html [nogin] Efficiency improvements._ Mon Sep 19 02:23:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-23-54-014138000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-23-54-014138000-PDT.html [nogin] Another 2_ on p4.ml_ Mon Sep 19 02:23:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-23-54-562007000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-23-54-562007000-PDT.html [jyh] Planning for update to .prla files._ Mon Sep 19 02:23:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-23-55-007408000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-23-55-007408000-PDT.html [jyh] Most of the theories in Itt now expand without errors._ Mon Sep 19 02:23:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-23-56-005874000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-23-56-005874000-PDT.html [nogin] I hope I finally got it right_ Mon Sep 19 02:29:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-29-41-526409000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-29-41-526409000-PDT.html [nogin] Moved the expand_itt test into tests directory_ Mon Sep 19 02:29:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-29-42-230644000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-29-42-230644000-PDT.html [nogin] Efficiency_ another 3_ on f650.ml_ Mon Sep 19 02:29:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-29-42-631750000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-29-42-631750000-PDT.html [nogin] There is no need to call dest_msequent when we only want the goal, but_ Mon Sep 19 02:29:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-29-43-035045000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-29-43-035045000-PDT.html [nogin] Efficiency_ Another 6_ on p4.ml_ Mon Sep 19 02:29:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-29-44-713997000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-29-44-713997000-PDT.html [nogin] Scripts for running ultiple tests in a batch._ Mon Sep 19 02:29:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-29-45-106261000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-02/2005-09-19-02-29-45-106261000-PDT.html