Wed, 01 Jun 2011 10:29:43 +0200 blanchet ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on
Wed, 01 Jun 2011 10:29:43 +0200 blanchet fixed interaction between type tags and hAPP in reconstruction code
Wed, 01 Jun 2011 10:29:43 +0200 blanchet implemented missing hAPP and ti cases of new path finder
Wed, 01 Jun 2011 10:29:43 +0200 blanchet support lightweight tags in new Metis
Wed, 01 Jun 2011 10:29:43 +0200 blanchet tuned names
Wed, 01 Jun 2011 10:29:43 +0200 blanchet export one more function
Wed, 01 Jun 2011 10:29:43 +0200 blanchet clausify "<=>" (needed for some type information)
Wed, 01 Jun 2011 10:29:43 +0200 blanchet distinguish different kinds of typing informations in the fact name
Wed, 01 Jun 2011 09:10:13 +0200 bulwahn splitting RBT theory into RBT and RBT_Mapping
Wed, 01 Jun 2011 08:07:28 +0200 bulwahn creating a free variable with proper name and local mixfix syntax (cf. db9b9e46131c)
Wed, 01 Jun 2011 08:07:27 +0200 bulwahn code preprocessor applies simplifier when schematic variables are fixed to free variables to allow rewriting with congruence rules in the preprocessing steps
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
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip