Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_translate.ML
Thu, 14 Jul 2011 17:29:30 +0200 blanchet move error logic closer to user file | diff | annotate
Thu, 14 Jul 2011 16:50:05 +0200 blanchet move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators) file | diff | annotate
Thu, 14 Jul 2011 16:50:05 +0200 blanchet added option to control which lambda translation to use (for experiments) file | diff | annotate
Wed, 06 Jul 2011 17:19:34 +0100 blanchet make SML/NJ happier file | diff | annotate
Wed, 06 Jul 2011 17:19:34 +0100 blanchet make SML/NJ happy + tuning file | diff | annotate
Tue, 05 Jul 2011 17:09:59 +0100 nik improved translation of lambdas in THF file | diff | annotate
Tue, 05 Jul 2011 17:09:59 +0100 nik added generation of lambdas in THF file | diff | annotate
Tue, 05 Jul 2011 17:09:59 +0100 nik add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order) file | diff | annotate
Fri, 01 Jul 2011 15:53:38 +0200 blanchet further repair "mangled_tags", now that tags are also mangled file | diff | annotate
Fri, 01 Jul 2011 15:53:38 +0200 blanchet renamed "type_sys" to "type_enc", which is more accurate file | diff | annotate
Fri, 01 Jul 2011 15:53:37 +0200 blanchet cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company file | diff | annotate
Fri, 01 Jul 2011 15:53:37 +0200 blanchet mangle "ti" tags file | diff | annotate
Fri, 01 Jul 2011 15:53:37 +0200 blanchet tuning file | diff | annotate
Mon, 27 Jun 2011 14:56:28 +0200 blanchet added "sound" option to force Sledgehammer to be pedantically sound file | diff | annotate
Tue, 21 Jun 2011 17:17:39 +0200 blanchet don't change the way helpers are generated for the exporter's sake file | diff | annotate
Tue, 21 Jun 2011 17:17:39 +0200 blanchet remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations file | diff | annotate
Tue, 21 Jun 2011 17:17:39 +0200 blanchet avoid double ASCII-fication file | diff | annotate
Tue, 21 Jun 2011 17:17:39 +0200 blanchet generate type predicates for existentials/skolems, otherwise some problems might not be provable file | diff | annotate
Thu, 16 Jun 2011 13:50:35 +0200 blanchet gave up an optimization that sometimes lead to unsound proofs -- in short, facts talking about a schematic type variable can encode a cardinality constraint and be consistent with HOL, e.g. "card (UNIV::?'a set) = 1 ==> ALL x y. x = y" file | diff | annotate
Thu, 16 Jun 2011 13:50:35 +0200 blanchet fixed soundness bug related to extensionality file | diff | annotate
Wed, 15 Jun 2011 14:36:41 +0200 blanchet fixed soundness bug made more visible by previous change file | diff | annotate
Wed, 15 Jun 2011 14:36:41 +0200 blanchet type arguments now (unlike back when fa2cf11d6351 was done) normally carry enough information to reconstruct the type of an applied constant, so no need to constraint the argument types in those cases file | diff | annotate
Fri, 10 Jun 2011 17:52:09 +0200 blanchet name tuning file | diff | annotate
Fri, 10 Jun 2011 17:52:09 +0200 blanchet revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug file | diff | annotate
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect; file | diff | annotate
Thu, 09 Jun 2011 00:16:28 +0200 blanchet cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices) file | diff | annotate
Wed, 08 Jun 2011 22:13:49 +0200 wenzelm merged file | diff | annotate
Wed, 08 Jun 2011 16:20:19 +0200 blanchet pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types file | diff | annotate
Wed, 08 Jun 2011 16:20:18 +0200 blanchet made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded file | diff | annotate
Wed, 08 Jun 2011 16:20:18 +0200 blanchet fixed format selection logic for Waldmeister file | diff | annotate
Wed, 08 Jun 2011 17:49:01 +0200 wenzelm updated headers; file | diff | annotate
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript; file | diff | annotate
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
less more (0) -60 tip
isabelle