src/HOL/Tools/Sledgehammer/metis_tactics.ML
2010-04-24 blanchet 2010-04-24 better error reporting; in particular, users shouldn't panic if "metis" can prove "False", especially in "neg_clausify"-style proofs
2010-04-19 blanchet 2010-04-19 added warning about inconsistent context to Metis; it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent
2010-04-16 blanchet 2010-04-16 added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
2010-04-16 blanchet 2010-04-16 store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
2010-04-15 blanchet 2010-04-15 give more sensible names to "fol_type" constructors, as requested by a FIXME comment
2010-03-28 wenzelm 2010-03-28 static defaults for configuration options;
2010-03-19 blanchet 2010-03-19 more Sledgehammer refactoring
2010-03-17 blanchet 2010-03-17 renamed Sledgehammer structures
2010-03-17 blanchet 2010-03-17 move Sledgehammer files in a directory of their own