[nogin] Wrote a section on MetaPRL exception_handling conventions._ Mon Sep 19 02:31:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-12-857335000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-12-857335000-PDT.html [nogin] ._ Mon Sep 19 02:31:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-13-286183000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-13-286183000-PDT.html [krupski] Small correction in term_core variants_ Mon Sep 19 02:31:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-13-712221000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-13-712221000-PDT.html [nogin] Removed some of the junk that Netscape added._ Mon Sep 19 02:31:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-14-126692000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-14-126692000-PDT.html [nogin] Define type inference types only once, not in 5 places._ Mon Sep 19 02:31:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-14-547345000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-14-547345000-PDT.html [nogin] Smarter type inference algorithm capable of doing things like_ Mon Sep 19 02:31:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-16-333853000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-16-333853000-PDT.html [nogin] Added iff handling for Jprover and Barber example_ Mon Sep 19 02:31:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-18-972281000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-18-972281000-PDT.html [nogin] Small Jprover___MetaPRL interface fix _ do not thin out universal_ Mon Sep 19 02:31:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-19-376218000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-19-376218000-PDT.html [steph] _ Mon Sep 19 02:31:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-19-799644000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-19-799644000-PDT.html [steph] _ Mon Sep 19 02:31:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-20-431314000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-20-431314000-PDT.html [nogin] let variable _ expression in_ Mon Sep 19 02:31:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-20-924933000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-20-924933000-PDT.html [nogin] Added gen_prover that Stephan forgot to commit._ Mon Sep 19 02:31:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-22-482376000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-22-482376000-PDT.html [nogin] I wrote a proof tree normalization that tries to eliminate unnecessary nodes_ Mon Sep 19 02:31:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-23-008255000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-23-008255000-PDT.html [nogin] I reformatted the TODO file from Emacs _outline_ mode to a numbered text file._ Mon Sep 19 02:31:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-25-282073000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-25-282073000-PDT.html [nogin] Numerous updates._ Mon Sep 19 02:31:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-25-698684000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-25-698684000-PDT.html [nogin] Changes I_ve made at CADE_ Further prof browsing improvements and others._ Mon Sep 19 02:31:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-26-866696000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-26-866696000-PDT.html [nogin] assumT shouldn_t run assertT when the conclusion is already what we want._ Mon Sep 19 02:31:27 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-27-714053000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-06/2005-09-19-02-31-27-714053000-PDT.html