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
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-14 blanchet 2011-04-14 tuning
2011-03-24 blanchet 2011-03-24 clean up new Skolemizer code -- some old hacks are no longer necessary
2011-03-24 blanchet 2011-03-24 more robust handling of variables in new Skolemizer
2011-01-10 wenzelm 2011-01-10 eliminated Int.toString;
2010-12-15 blanchet 2010-12-15 tuning
2010-12-15 blanchet 2010-12-15 added Sledgehammer support for higher-order propositional reasoning
2010-12-15 blanchet 2010-12-15 add Metis support for higher-order propositional reasoning
2010-12-15 blanchet 2010-12-15 implemented partially-typed "tags" type encoding
2010-10-29 blanchet 2010-10-29 prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
2010-10-26 blanchet 2010-10-26 renaming
2010-10-26 blanchet 2010-10-26 no need to encode theorem number twice in skolem names
2010-10-06 blanchet 2010-10-06 qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
2010-10-05 blanchet 2010-10-05 tuned comments
2010-10-05 blanchet 2010-10-05 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
2010-10-04 blanchet 2010-10-04 move Metis into Plain