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
2006-08-02 wenzelm 2006-08-02 simplified Assumption/ProofContext.export;
2006-07-16 paulson 2006-07-16 has_consts renamed to has_conn, now actually parses the first-order formula to avoid problems caused by connectives buried within descriptions and set comprehensions.
2006-07-13 paulson 2006-07-13 fix to refl_clause_aux: added occurs check
2006-07-11 wenzelm 2006-07-11 removed obsolete mem_term;
2006-07-05 paulson 2006-07-05 removed the "tagging" feature
2006-06-15 paulson 2006-06-15 the "all_theorems" option and some fixes
2006-06-13 wenzelm 2006-06-13 avoid unqualified exception names; tuned;
2006-05-26 wenzelm 2006-05-26 freeze_spec: gensym;
2006-03-07 paulson 2006-03-07 Tidying, and getting rid of SELECT_GOAL (as it does something different now)
2006-02-28 paulson 2006-02-28 fixed but in freeze_spec
2006-02-20 paulson 2006-02-20 Fix variable-naming bug (?) by removing a needless recursive call
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-01-28 wenzelm 2006-01-28 LocalDefs.def_export;
2006-01-23 paulson 2006-01-23 Clausification now handles some IFs in rewrite rules (if-split did not work)
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 Output.debug;
2006-01-13 wenzelm 2006-01-13 ProofContext.def_export;
2005-12-23 paulson 2005-12-23 tidied
2005-12-14 paulson 2005-12-14 removal of some redundancies (e.g. one-point-rules) in clause production
2005-12-13 paulson 2005-12-13 removal of functional reflexivity axioms
2005-11-18 mengj 2005-11-18 -- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL. -- added "check_is_fol_term", which is the same as "check_is_fol", but takes a "term" as input. -- added "check_is_fol" and "check_is_fol_term" into the signature.
2005-11-16 paulson 2005-11-16 new version of "tryres" allowing multiple unifiers (apparently needed for Skolemization of higher-order theorems)
2005-11-09 paulson 2005-11-09 Skolemization by inference, but not quite finished
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop;
2005-10-14 paulson 2005-10-14 signature changes
2005-09-29 paulson 2005-09-29 moved concat_with_and to watcher.ML
2005-09-15 paulson 2005-09-15 the experimental tagging system, and the usual tidying