2007-05-10 wenzelm 2007-05-10 moved some Drule operations to Thm (see more_thm.ML);
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-19 paulson 2007-04-19 trying to make single-step proofs work better, especially if they contain abstraction functions. Uniform names for Skolem and Abstraction functions
2007-04-18 paulson 2007-04-18 Fixes for proof reconstruction, especially involving abstractions and definitions
2007-04-15 wenzelm 2007-04-15 Thm.fold_terms;
2007-04-12 paulson 2007-04-12 Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-03-26 paulson 2007-03-26 Clause cache is now in theory data. Deleted skolem_use_cache_thm, so cnf_rules_of_ths now calls cnf_axiom.
2007-03-19 paulson 2007-03-19 Removal of axiom names from the theorem cache
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-22 paulson 2007-02-22 Improved handling of situation when theorem in cache disagrees with theorem supplied: new clauses are now returned, fixing a bug in the metis method.
2007-01-31 haftmann 2007-01-31 dropped lemma duplicates in HOL.thy
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-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-11-30 wenzelm 2006-11-30 Goal.norm/close_result;
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic; tuned;
2006-11-22 paulson 2006-11-22 Consolidation of code to "blacklist" unhelpful theorems, including record surjectivity properties
2006-11-21 paulson 2006-11-21 New transformation of eliminatino rules: we simply replace the final conclusion variable by False
2006-11-10 paulson 2006-11-10 Improvement to classrel clauses: now outputs the minimum needed. Theorem names: trying to minimize the number of multiple theorem names presented
2006-11-08 wenzelm 2006-11-08 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
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 meson method MUST NOT use all safe rules, only basic ones for the logical connectives.
2006-10-20 paulson 2006-10-20 Fixed the "exception Empty" bug in elim2Fol Also added a check to suppress elimination rules that would yield too many clauses More debugging info
2006-10-12 paulson 2006-10-12 abstraction is now turned OFF...
2006-10-11 paulson 2006-10-11 Abstraction re-use code now checks that the abstraction function can be used in the current theory.
2006-10-09 wenzelm 2006-10-09 replaced Drule.clhs/crhs_of by Drule.lhs/rhs_of;
2006-10-06 paulson 2006-10-06 Refinements to abstraction. Seeding with combinators K, I and B.
2006-10-05 paulson 2006-10-05 improvements to abstraction, ensuring more re-use of abstraction functions moving some functions to Pure/drule.ML
2006-09-30 mengj 2006-09-30 Removed ResHolClause.LAM2COMB exception.
2006-09-29 wenzelm 2006-09-29 Sign.add_consts_authentic;
2006-09-28 wenzelm 2006-09-28 ResAtpset.get_atpset;
2006-09-26 paulson 2006-09-26 Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
2006-09-19 wenzelm 2006-09-19 sko/abs: Name.internal prevents choking of print_theory;
2006-09-18 paulson 2006-09-18 Bug fix to prevent exception dest_Free from escaping
2006-09-13 paulson 2006-09-13 bug fix to abstractions: free variables in theorem can be abstracted over.
2006-09-04 paulson 2006-09-04 Using Drule.local_standard to reduce the space usage
2006-09-01 wenzelm 2006-09-01 skolem_cache_thm: Drule.close_derivation on clauses preserves some space; tuned skolem_cache operations: canonical argument order; tuned monomorphic test;
2006-09-01 paulson 2006-09-01 refinements to conversion into clause form, esp for the HO case
2006-08-31 paulson 2006-08-31 improvements to abstraction generation
2006-08-28 paulson 2006-08-28 tidied
2006-08-25 paulson 2006-08-25 abstraction of lambda-expressions
2006-08-09 paulson 2006-08-09 consistent prefixing for skolem functions
2006-08-08 paulson 2006-08-08 skolem declarations for built-in theorems
2006-08-02 wenzelm 2006-08-02 removed obsolete Drule.freeze_all -- now uses legacy Drule.freeze_thaw;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-05 paulson 2006-07-05 made the conversion of elimination rules more robust
2006-06-15 paulson 2006-06-15 the "all_theorems" option and some fixes
2006-05-13 wenzelm 2006-05-13 Theory.add_defs(_i): added unchecked flag;
2006-04-18 mengj 2006-04-18 Tidied up some programs.
2006-04-07 mengj 2006-04-07 added another function for CNF.
2006-03-10 paulson 2006-03-10 Changed some warnings to debug messages
2006-03-07 paulson 2006-03-07 Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before. Removal of the unused err_list.
2006-03-07 mengj 2006-03-07 Added functions to retrieve local and global atpset rules. cnf thms to Term.term format.
2006-03-02 paulson 2006-03-02 subset_refl now included using the atp attribute
2006-02-20 paulson 2006-02-20 Inclusion of subset_refl in ATP calls
2006-02-03 paulson 2006-02-03 removal of case analysis clauses