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