src/HOL/Tools/Metis/metis_translate.ML
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