src/HOL/Tools/Metis/metis_translate.ML
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
2011-06-08 blanchet 2011-06-08 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
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"
2011-06-07 blanchet 2011-06-07 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
2011-06-07 blanchet 2011-06-07 removed "verbose" option -- there won't be any verbosity in there, according to Sascha (yeah)
2011-06-07 blanchet 2011-06-07 nicely thread monomorphism verbosity in Metis and Sledgehammer
2011-06-07 blanchet 2011-06-07 renamed ML function
2011-06-06 blanchet 2011-06-06 Metis code cleanup
2011-06-06 blanchet 2011-06-06 enable new Metis
2011-06-06 blanchet 2011-06-06 more preparations towards hijacking Metis
2011-06-06 blanchet 2011-06-06 make "metisX"'s default more like old "metis"
2011-06-06 blanchet 2011-06-06 fixed type helper indices in new Metis
2011-06-06 blanchet 2011-06-06 improved ATP clausifier so it can deal with "x => (y <=> z)"
2011-06-06 blanchet 2011-06-06 don't translate new Skolemizer assumptions in new Metis
2011-06-06 blanchet 2011-06-06 tuning
2011-06-06 blanchet 2011-06-06 conceal old Skolems in new Metis
2011-06-06 blanchet 2011-06-06 properly locate helpers whose constants have several entries in the helper table
2011-06-06 blanchet 2011-06-06 skip "hBOOL" in new Metis path finder
2011-06-06 blanchet 2011-06-06 don't pass "~ " to new Metis
2011-06-06 blanchet 2011-06-06 clean up unnecessary machinery -- helpers work also with monomorphic type encodings
2011-06-06 blanchet 2011-06-06 added support for helpers in new Metis, so far only for polymorphic type encodings
2011-06-01 blanchet 2011-06-01 ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on
2011-06-01 blanchet 2011-06-01 implemented missing hAPP and ti cases of new path finder
2011-06-01 blanchet 2011-06-01 support lightweight tags in new Metis
2011-06-01 blanchet 2011-06-01 tuned names
2011-06-01 blanchet 2011-06-01 distinguish different kinds of typing informations in the fact name
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 fixed new path finder for type information tag
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 parse optional type system specification
2011-05-31 blanchet 2011-05-31 proper handling of type variable classes in new Metis
2011-05-31 blanchet 2011-05-31 don't preprocess twice
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 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-27 blanchet 2011-05-27 tuning
2011-05-27 blanchet 2011-05-27 cleaner handling of equality and proxies (esp. for THF)
2011-05-20 blanchet 2011-05-20 name tuning
2011-05-20 blanchet 2011-05-20 further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged
2011-05-20 blanchet 2011-05-20 prevent unsound combinator proofs in partially typed polymorphic type systems
2011-05-20 blanchet 2011-05-20 tuning
2011-05-12 blanchet 2011-05-12 handle equality proxy in a more backward-compatible way
2011-05-12 blanchet 2011-05-12 reenabled equality proxy in Metis for higher-order reasoning
2011-05-12 blanchet 2011-05-12 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
2011-05-03 blanchet 2011-05-03 reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
2011-05-01 blanchet 2011-05-01 drop "fequal" type args for unmangled type systems
2011-05-01 blanchet 2011-05-01 cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
2011-05-01 blanchet 2011-05-01 improve helper type instantiation code
2011-05-01 blanchet 2011-05-01 killed needless datatype "combtyp" in Metis
2011-05-01 blanchet 2011-05-01 have properly type-instantiated helper facts (combinators and If)
2011-05-01 blanchet 2011-05-01 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
2011-05-01 blanchet 2011-05-01 no point in keeping indices in Sledgehammer readable var names, since these are disambiguated anyway
2011-05-01 blanchet 2011-05-01 added more rudimentary type support to Sledgehammer's ATP encoding