src/HOL/Tools/metis_tools.ML
2007-10-10 paulson 2007-10-10 getting rid of type typ_var
2007-10-09 paulson 2007-10-09 context-based treatment of generalization; also handling TFrees in axiom clauses
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-05 paulson 2007-10-05 metis method: used theorems
2007-10-04 paulson 2007-10-04 combinator translation
2007-08-31 wenzelm 2007-08-31 type_infer: mode_pattern;
2007-08-30 wenzelm 2007-08-30 replaced ProofContext.infer_types by general Syntax.check_terms; use Variable.polymorphic to get schematic type variables;
2007-08-24 paulson 2007-08-24 Reconstruction bug fix
2007-08-18 wenzelm 2007-08-18 export more tactics; ResHolClause.literals_of_term: proper theory argument; removed obsolete ResClause.init, ResHolClause.init;
2007-08-17 wenzelm 2007-08-17 turned type_lits into configuration option (with attribute);
2007-08-17 wenzelm 2007-08-17 proper signature for Meson;
2007-07-29 wenzelm 2007-07-29 metis_tac: proper context (ProofContext.init it *not* sufficient); simplified method setup;
2007-06-20 wenzelm 2007-06-20 tuned comments;
2007-06-20 wenzelm 2007-06-20 The Metis prover (slightly modified version from Larry);