src/HOL/Tools/metis_tools.ML
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-18 wenzelm 2009-10-18 removed some unreferenced material; tuned;
2009-10-16 wenzelm 2009-10-16 tuned white space;
2009-10-16 wenzelm 2009-10-16 local channels for tracing/debugging;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-07 paulson 2009-09-07 Fixed a few problems with the method metisFT
2009-09-07 paulson 2009-09-07 My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
2009-09-07 paulson 2009-09-07 conflict resolution possibly
2009-09-04 paulson 2009-09-04 New method, metisFT: a fully-typed proof search that should eliminate type errors during reconstruction
2009-08-28 wenzelm 2009-08-28 modernized messages -- eliminated ctyp/cterm operations;
2009-07-29 wenzelm 2009-07-29 Meson.first_order_resolve: avoid handle _; proper context for various Meson and Metis rules and tactics unified meson_tac/meson_claset_tac;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-08 wenzelm 2009-03-08 more explicit warning message;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2008-12-31 wenzelm 2008-12-31 use regular Term.add_vars, Term.add_frees etc.; moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-10-28 paulson 2008-10-28 The metis method no longer fails because the theorem is too trivial
2008-10-08 paulson 2008-10-08 The result of the equality inference rule no longer undergoes factoring.
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-09-16 paulson 2008-09-16 The metis method now fails in the usual manner, rather than raising an exception, if it determines that it cannot prove the theorem.
2008-09-09 paulson 2008-09-09 Overall exception handler in order to insulate our users from low-level bugs.
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-16 wenzelm 2008-06-16 RuleInsts.read_instantiate;
2008-06-12 wenzelm 2008-06-12 ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
2008-06-11 wenzelm 2008-06-11 Drule.read_instantiate;
2008-05-18 wenzelm 2008-05-18 eliminated theory CPure;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 cat_lines;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-07 paulson 2008-04-07 Superficial changes CVS: ----------------------------------------------------------------------
2008-03-27 wenzelm 2008-03-27 removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
2008-01-02 paulson 2008-01-02 testing for empty sort
2007-12-20 wenzelm 2007-12-20 made refute non-critical (seems to work after avoiding floating point random numbers);
2007-12-19 wenzelm 2007-12-19 removed duplicate CRITICAL markup;
2007-12-19 paulson 2007-12-19 Replaced refs by config params; finer critical section in mets method
2007-12-19 wenzelm 2007-12-19 marked refute (the main metis procedure) as CRITICAL;
2007-12-18 paulson 2007-12-18 Deleted redundant setmp calls
2007-10-11 paulson 2007-10-11 reconstruction bug fix
2007-10-11 paulson 2007-10-11 rationalized redundant code
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);