2011-05-31 boehmes 2011-05-31 use new monomorphizer for SMT; simplify the monomorphizer by inlining functions and proper passing of arguments
2011-05-31 bulwahn 2011-05-31 merged
2011-05-31 bulwahn 2011-05-31 Quickcheck Narrowing only requires one compilation with GHC now
2011-05-31 bulwahn 2011-05-31 splitting test_goal_terms in Quickcheck into smaller basic functions
2011-05-31 bulwahn 2011-05-31 adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
2011-05-31 blanchet 2011-05-31 compile
2011-05-31 blanchet 2011-05-31 compile
2011-05-31 blanchet 2011-05-31 monomorphize in the new Metis if the type system calls for it
2011-05-31 blanchet 2011-05-31 use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
2011-05-31 blanchet 2011-05-31 fixed comment
2011-05-31 blanchet 2011-05-31 fixed new path finder for type information tag
2011-05-31 blanchet 2011-05-31 no need for type arguments with "xxx_tags_heavy" type system
2011-05-31 blanchet 2011-05-31 use ":" for type information (looks good in Metis's output) and handle it in new path finder
2011-05-31 blanchet 2011-05-31 tuned name
2011-05-31 blanchet 2011-05-31 tuned name
2011-05-31 blanchet 2011-05-31 make "prepare_atp_problem" more robust w.r.t. choice of type system
2011-05-31 blanchet 2011-05-31 parse optional type system specification
2011-05-31 blanchet 2011-05-31 tuning
2011-05-31 blanchet 2011-05-31 proper handling of type variable classes in new Metis
2011-05-31 blanchet 2011-05-31 fixed recursive call in new path finder and (untested:) handle hAPP
2011-05-31 blanchet 2011-05-31 don't preprocess twice
2011-05-31 blanchet 2011-05-31 more robust and simpler adjustment computation
2011-05-31 blanchet 2011-05-31 more work on new Metis
2011-05-31 blanchet 2011-05-31 tuning
2011-05-31 blanchet 2011-05-31 more work on new metis that exploits the powerful new type encodings
2011-05-31 blanchet 2011-05-31 tuning
2011-05-31 blanchet 2011-05-31 removed obscure option
2011-05-31 blanchet 2011-05-31 added "metisX" syntax (temporary)
2011-05-31 blanchet 2011-05-31 compile
2011-05-31 blanchet 2011-05-31 added new metis mode, with no implementation yet
2011-05-31 blanchet 2011-05-31 tuning
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation
2011-05-31 krauss 2011-05-31 more precise authorship, reflecting my own ignorance and hg annotate
2011-05-31 krauss 2011-05-31 generate raw induction rule as instance of generic rule with careful treatment of currying
2011-05-31 krauss 2011-05-31 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
2011-05-31 krauss 2011-05-31 admissibility on option type
2011-05-23 krauss 2011-05-23 also manage induction rule; tuned data slot
2011-05-30 bulwahn 2011-05-30 improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
2011-05-30 paulson 2011-05-30 merged
2011-05-30 paulson 2011-05-30 Workaround for bug involving makeindex, hyperref and the | symbol
2011-05-30 krauss 2011-05-30 parameterize print_theorems over actual search function
2011-05-30 krauss 2011-05-30 added experimental yxml_find_theorems web service (but no client yet)
2011-05-30 krauss 2011-05-30 generic ScgiServer.simple_handler
2011-05-30 krauss 2011-05-30 moved html templates to a separate module, making their awkward signatures explicit
2011-05-30 krauss 2011-05-30 attempt to clarify code; removed "handle _" and dead code
2011-05-30 krauss 2011-05-30 (de)serialization for search query and result
2011-05-30 krauss 2011-05-30 explicit type for search queries
2011-05-30 krauss 2011-05-30 moved questionable goal modification out of filter_theorems
2011-05-30 krauss 2011-05-30 exported raw query parser; removed inconsistent clone
2011-05-30 krauss 2011-05-30 separate query parsing from actual search
2011-05-30 blanchet 2011-05-30 fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
2011-05-30 blanchet 2011-05-30 document new explicit apply
2011-05-30 blanchet 2011-05-30 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
2011-05-30 blanchet 2011-05-30 don't slice if there are too few facts
2011-05-30 blanchet 2011-05-30 nicer failure message when one-line proof reconstruction fails
2011-05-30 blanchet 2011-05-30 make SML/NJ happy
2011-05-30 blanchet 2011-05-30 avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
2011-05-30 blanchet 2011-05-30 make all messages urgent in verbose mode
2011-05-30 blanchet 2011-05-30 minimize automatically even if Metis failed, if the external prover was really fast
2011-05-30 blanchet 2011-05-30 fixed syntax of min options