Mercurialisabelle / file revisions
summary | shortlog | changelog | graph | tags | branches | file | revisions | annotate | diff | rss
src/HOL/Tools/ATP/atp_translate.ML
2011-07-17 blanchet 2011-07-17 fixed lambda-liftg: must ensure the formulas are in close form file | diff | annotate
2011-07-17 blanchet 2011-07-17 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names) file | diff | annotate
2011-07-17 blanchet 2011-07-17 pass kind to lambda-translation function file | diff | annotate
2011-07-17 blanchet 2011-07-17 more refactoring of preprocessing file | diff | annotate
2011-07-17 blanchet 2011-07-17 more refactoring of preprocessing, so as to be able to centralize it file | diff | annotate
2011-07-17 blanchet 2011-07-17 renamed internal data structure file | diff | annotate
2011-07-17 blanchet 2011-07-17 simplify code -- there are no lambdas in helpers anyway file | diff | annotate
2011-07-17 blanchet 2011-07-17 added lambda-lifting to Sledgehammer (rough) file | diff | annotate
2011-07-17 blanchet 2011-07-17 move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons file | diff | annotate
2011-07-14 blanchet 2011-07-14 move error logic closer to user file | diff | annotate
2011-07-14 blanchet 2011-07-14 move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators) file | diff | annotate
2011-07-14 blanchet 2011-07-14 added option to control which lambda translation to use (for experiments) file | diff | annotate
2011-07-06 blanchet 2011-07-06 make SML/NJ happier file | diff | annotate
2011-07-06 blanchet 2011-07-06 make SML/NJ happy + tuning file | diff | annotate
2011-07-05 nik 2011-07-05 improved translation of lambdas in THF file | diff | annotate
2011-07-05 nik 2011-07-05 added generation of lambdas in THF file | diff | annotate
2011-07-05 nik 2011-07-05 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order) file | diff | annotate
2011-07-01 blanchet 2011-07-01 further repair "mangled_tags", now that tags are also mangled file | diff | annotate
2011-07-01 blanchet 2011-07-01 renamed "type_sys" to "type_enc", which is more accurate file | diff | annotate
2011-07-01 blanchet 2011-07-01 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
2011-07-01 blanchet 2011-07-01 mangle "ti" tags file | diff | annotate
2011-07-01 blanchet 2011-07-01 tuning file | diff | annotate
2011-06-27 blanchet 2011-06-27 added "sound" option to force Sledgehammer to be pedantically sound file | diff | annotate
2011-06-21 blanchet 2011-06-21 don't change the way helpers are generated for the exporter's sake file | diff | annotate
2011-06-21 blanchet 2011-06-21 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations file | diff | annotate
2011-06-21 blanchet 2011-06-21 avoid double ASCII-fication file | diff | annotate
2011-06-21 blanchet 2011-06-21 generate type predicates for existentials/skolems, otherwise some problems might not be provable file | diff | annotate
2011-06-16 blanchet 2011-06-16 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
2011-06-16 blanchet 2011-06-16 fixed soundness bug related to extensionality file | diff | annotate
2011-06-15 blanchet 2011-06-15 fixed soundness bug made more visible by previous change file | diff | annotate
2011-06-15 blanchet 2011-06-15 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
2011-06-10 blanchet 2011-06-10 name tuning file | diff | annotate
2011-06-10 blanchet 2011-06-10 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug file | diff | annotate
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect; file | diff | annotate
2011-06-09 blanchet 2011-06-09 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
2011-06-08 wenzelm 2011-06-08 merged file | diff | annotate
2011-06-08 blanchet 2011-06-08 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
2011-06-08 blanchet 2011-06-08 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
2011-06-08 blanchet 2011-06-08 fixed format selection logic for Waldmeister file | diff | annotate
2011-06-08 wenzelm 2011-06-08 updated headers; file | diff | annotate
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript; file | diff | annotate
2011-06-08 blanchet 2011-06-08 minor optimization file | diff | annotate
2011-06-08 blanchet 2011-06-08 don't needlessly extensionalize file | diff | annotate
2011-06-08 blanchet 2011-06-08 don't needlessly presimplify -- makes ATP problem preparation much faster file | diff | annotate
2011-06-08 blanchet 2011-06-08 tuned file | diff | annotate
2011-06-08 blanchet 2011-06-08 killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true" file | diff | annotate
2011-06-08 blanchet 2011-06-08 slightly faster/cleaner accumulation of polymorphic consts file | diff | annotate
2011-06-07 blanchet 2011-06-07 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs file | diff | annotate
2011-06-07 blanchet 2011-06-07 pass props not thms to ATP translator file | diff | annotate
2011-06-06 blanchet 2011-06-06 removed old optimization that isn't one anyone file | diff | annotate
2011-06-06 blanchet 2011-06-06 generate less type information in polymorphic case file | diff | annotate
2011-06-06 blanchet 2011-06-06 made "explicit_apply"'s smart mode (more) complete file | diff | annotate
2011-06-06 blanchet 2011-06-06 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
2011-06-06 blanchet 2011-06-06 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s file | diff | annotate
2011-06-06 blanchet 2011-06-06 whitespace tuning file | diff | annotate
2011-06-06 blanchet 2011-06-06 fixed type helper indices in new Metis file | diff | annotate
2011-06-06 blanchet 2011-06-06 improved ATP clausifier so it can deal with "x => (y <=> z)" file | diff | annotate
2011-06-06 blanchet 2011-06-06 avoid renumbering hypotheses file | diff | annotate
2011-06-06 blanchet 2011-06-06 tuning file | diff | annotate
2011-06-06 blanchet 2011-06-06 fixed detection of Skolem constants in type construction detection code file | diff | annotate
isabelle