2009-07-27 ago moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-17 ago tuned/modernized Envir operations;
2009-07-06 ago structure Thm: less pervasive names;
2009-06-04 ago dropped legacy ML bindings; tuned
2009-03-20 ago eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2009-03-01 ago use long names for old-style fold combinators;
2009-01-29 ago Minor reorganisation of the Skolemization code
2008-12-31 ago use exists_subterm directly;
2008-09-29 ago handle _ should be avoided (spurious Interrupt will spoil the game);
2008-09-09 ago more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
2008-08-14 ago moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-06-16 ago pervasive RuleInsts;
2008-06-16 ago RuleInsts.read_instantiate;
2008-06-11 ago Drule.read_instantiate;
2008-05-17 ago cat_lines;
2008-05-17 ago structure Display: less pervasive operations;
2008-04-07 ago * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
2008-03-27 ago eliminated theory ProtoPure;
2008-02-13 ago make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
2007-12-19 ago Replaced refs by config params; finer critical section in mets method
2007-12-18 ago Skolemization now catches exception THM, which may be raised if unification fails.
2007-10-09 ago context-based treatment of generalization; also handling TFrees in axiom clauses
2007-10-04 ago combinator translation
2007-09-27 ago removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
2007-08-17 ago proper signature for Meson;
2007-07-29 ago proper simproc_setup for "neq", "let_simp";
2007-07-21 ago tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
2007-07-05 ago renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-03 ago to handle non-atomic assumptions
2007-06-20 ago Added flexflex_first_order and tidied first_order_resolution
2007-06-05 ago eliminated Code_Generator.thy
2007-05-08 ago tuned;
2007-04-18 ago Fixes for proof reconstruction, especially involving abstractions and definitions
2007-04-12 ago Zero variable indexes in clauses
2007-03-29 ago MESON tactical takes an additional argument: the clausification function.
2007-03-26 ago "generalize" now replaces ugly mes_XXX generated symbols by 1-letter identifiers.
2007-03-02 ago The first-order test now tests for the obscure case of a polymorphic constant like 1 being
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-01-20 ago Output.debug: non-strict;
2007-01-04 ago improvements to proof reconstruction. Some files loaded in a different order
2006-12-22 ago tidying the ATP communications
2006-12-06 ago LocalDefs.expand;
2006-12-05 ago thm/prf: separate official name vs. additional tags;
2006-12-01 ago Fixed a MAJOR BUG in clause-counting: only Boolean equalities now count as iffs
2006-11-29 ago simplified method setup;
2006-11-04 ago removed is_Trueprop (use can dest_Trueprop'' instead);
2006-10-26 ago Conversion to clause form now tolerates Boolean variables without looping.
2006-10-23 ago Improved tracing
2006-10-20 ago nclauses no longer requires its input to be in NNF
2006-10-18 ago More robust error handling in make_nnf and forward_res
2006-10-16 ago moved HOL code generator setup to Code_Generator
2006-10-11 ago abandoned findrep
2006-10-02 ago Now checks explicitly for Trueprop, thereby ignoring junk theorems involving OF_CLASS, etc.
2006-09-13 ago Tweaks to is_fol_term, the first-order test. We don't count "=" as a connective
2006-08-25 ago better skolemization, using first-order resolution rather than hoping for the right result
2006-08-08 ago more explict variable names
2006-08-02 ago simplified Assumption/ProofContext.export;
2006-07-16 ago has_consts renamed to has_conn, now actually parses the first-order formula
2006-07-13 ago fix to refl_clause_aux: added occurs check