Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_translate.ML
Wed, 08 Jun 2011 08:47:43 +0200 blanchet minor optimization file | diff | annotate
Wed, 08 Jun 2011 08:47:43 +0200 blanchet don't needlessly extensionalize file | diff | annotate
Wed, 08 Jun 2011 08:47:43 +0200 blanchet don't needlessly presimplify -- makes ATP problem preparation much faster file | diff | annotate
Wed, 08 Jun 2011 08:47:43 +0200 blanchet tuned file | diff | annotate
Wed, 08 Jun 2011 08:47:43 +0200 blanchet killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true" file | diff | annotate
Wed, 08 Jun 2011 08:47:43 +0200 blanchet slightly faster/cleaner accumulation of polymorphic consts file | diff | annotate
Tue, 07 Jun 2011 14:17:35 +0200 blanchet more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs file | diff | annotate
Tue, 07 Jun 2011 06:58:52 +0200 blanchet pass props not thms to ATP translator file | diff | annotate
Mon, 06 Jun 2011 20:56:06 +0200 blanchet removed old optimization that isn't one anyone file | diff | annotate
Mon, 06 Jun 2011 20:56:06 +0200 blanchet generate less type information in polymorphic case file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet made "explicit_apply"'s smart mode (more) complete file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet change var name as a workaround for rare issue in Metis's reconstruction code -- namely, "find_var" fails because "X = X" is wrongly mirrorred as "A = A" file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet whitespace tuning file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet fixed type helper indices in new Metis file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet improved ATP clausifier so it can deal with "x => (y <=> z)" file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet avoid renumbering hypotheses file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuning file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet fixed detection of Skolem constants in type construction detection code file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't stumble on Skolem names file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't merge "hAPP"s even in unsound heavy modes, because "hAPP" then sometimes gets declared with too strict arguments ("ind"), and we lose some proofs file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet properly locate helpers whose constants have several entries in the helper table file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet skip "hBOOL" in new Metis path finder file | diff | annotate
Mon, 06 Jun 2011 20:36:34 +0200 blanchet ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis) file | diff | annotate
Mon, 06 Jun 2011 20:36:34 +0200 blanchet added support for helpers in new Metis, so far only for polymorphic type encodings file | diff | annotate
Wed, 01 Jun 2011 19:50:59 +0200 blanchet fixed debilitating translation bug introduced in b6e61d22fa61 -- "equal" and "=" should always have arity 2 file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet implemented missing hAPP and ti cases of new path finder file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet support lightweight tags in new Metis file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet tuned names file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet distinguish different kinds of typing informations in the fact name file | diff | annotate
Wed, 01 Jun 2011 00:23:16 +0200 blanchet make SML/NJ happier file | diff | annotate
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 file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet no need for type arguments with "xxx_tags_heavy" type system file | diff | annotate
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 file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet tuned name file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet make "prepare_atp_problem" more robust w.r.t. choice of type system file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet proper handling of type variable classes in new Metis file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet don't preprocess twice file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet more work on new metis that exploits the powerful new type encodings file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation file | diff | annotate | base
less more (0) tip
isabelle