Wed, 01 Jun 2011 00:23:16 +0200 blanchet make SML/NJ happier
Wed, 01 Jun 2011 00:12:38 +0200 blanchet make sure "Trueprop" is removed before combinators are added -- the code is fragile in that respect
Tue, 31 May 2011 23:39:27 +0200 blanchet speed up example by disabling preplay, and temporarily comment out a broken Sledgehammer call
Tue, 31 May 2011 19:28:03 +0200 boehmes updated SMT certificates
Tue, 31 May 2011 19:27:19 +0200 boehmes proper nesting of loops in new monomorphizer;
Tue, 31 May 2011 19:21:20 +0200 boehmes use new monomorphizer for SMT;
Tue, 31 May 2011 18:13:00 +0200 bulwahn merged
Tue, 31 May 2011 15:45:27 +0200 bulwahn Quickcheck Narrowing only requires one compilation with GHC now
Tue, 31 May 2011 15:45:26 +0200 bulwahn splitting test_goal_terms in Quickcheck into smaller basic functions
Tue, 31 May 2011 15:45:24 +0200 bulwahn adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
Tue, 31 May 2011 17:15:14 +0200 blanchet compile
Tue, 31 May 2011 17:05:44 +0200 blanchet compile
Tue, 31 May 2011 16:38:36 +0200 blanchet monomorphize in the new Metis if the type system calls for it
Tue, 31 May 2011 16:38:36 +0200 blanchet use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
Tue, 31 May 2011 16:38:36 +0200 blanchet fixed comment
Tue, 31 May 2011 16:38:36 +0200 blanchet fixed new path finder for type information tag
Tue, 31 May 2011 16:38:36 +0200 blanchet no need for type arguments with "xxx_tags_heavy" type system
Tue, 31 May 2011 16:38:36 +0200 blanchet use ":" for type information (looks good in Metis's output) and handle it in new path finder
Tue, 31 May 2011 16:38:36 +0200 blanchet tuned name
Tue, 31 May 2011 16:38:36 +0200 blanchet tuned name
Tue, 31 May 2011 16:38:36 +0200 blanchet make "prepare_atp_problem" more robust w.r.t. choice of type system
Tue, 31 May 2011 16:38:36 +0200 blanchet parse optional type system specification
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning
Tue, 31 May 2011 16:38:36 +0200 blanchet proper handling of type variable classes in new Metis
Tue, 31 May 2011 16:38:36 +0200 blanchet fixed recursive call in new path finder and (untested:) handle hAPP
Tue, 31 May 2011 16:38:36 +0200 blanchet don't preprocess twice
Tue, 31 May 2011 16:38:36 +0200 blanchet more robust and simpler adjustment computation
Tue, 31 May 2011 16:38:36 +0200 blanchet more work on new Metis
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning
Tue, 31 May 2011 16:38:36 +0200 blanchet more work on new metis that exploits the powerful new type encodings
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning
Tue, 31 May 2011 16:38:36 +0200 blanchet removed obscure option
Tue, 31 May 2011 16:38:36 +0200 blanchet added "metisX" syntax (temporary)
Tue, 31 May 2011 16:38:36 +0200 blanchet compile
Tue, 31 May 2011 16:38:36 +0200 blanchet added new metis mode, with no implementation yet
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation
Tue, 31 May 2011 11:21:47 +0200 krauss more precise authorship, reflecting my own ignorance and hg annotate
Tue, 31 May 2011 11:16:52 +0200 krauss generate raw induction rule as instance of generic rule with careful treatment of currying
Tue, 31 May 2011 11:16:34 +0200 krauss generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
Tue, 31 May 2011 11:11:17 +0200 krauss admissibility on option type
Mon, 23 May 2011 21:34:37 +0200 krauss also manage induction rule;
Mon, 30 May 2011 17:55:34 +0200 bulwahn improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
Mon, 30 May 2011 16:15:37 +0100 paulson merged
Mon, 30 May 2011 16:10:12 +0100 paulson Workaround for bug involving makeindex, hyperref and the | symbol
Mon, 30 May 2011 17:07:48 +0200 krauss parameterize print_theorems over actual search function
Mon, 30 May 2011 17:07:48 +0200 krauss added experimental yxml_find_theorems web service (but no client yet)
Mon, 30 May 2011 17:07:48 +0200 krauss generic ScgiServer.simple_handler
Mon, 30 May 2011 17:07:48 +0200 krauss moved html templates to a separate module, making their awkward signatures explicit
Mon, 30 May 2011 17:07:48 +0200 krauss attempt to clarify code; removed "handle _" and dead code
Mon, 30 May 2011 17:07:48 +0200 krauss (de)serialization for search query and result
Mon, 30 May 2011 17:07:48 +0200 krauss explicit type for search queries
Mon, 30 May 2011 17:07:48 +0200 krauss moved questionable goal modification out of filter_theorems
Mon, 30 May 2011 17:07:48 +0200 krauss exported raw query parser; removed inconsistent clone
Mon, 30 May 2011 17:07:48 +0200 krauss separate query parsing from actual search
Mon, 30 May 2011 17:00:38 +0200 blanchet fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
Mon, 30 May 2011 17:00:38 +0200 blanchet document new explicit apply
Mon, 30 May 2011 17:00:38 +0200 blanchet made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
Mon, 30 May 2011 17:00:38 +0200 blanchet don't slice if there are too few facts
Mon, 30 May 2011 17:00:38 +0200 blanchet nicer failure message when one-line proof reconstruction fails
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip