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
2006-01-29 wenzelm 2006-01-29 tuned comment;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 Output.debug;
2006-01-10 wenzelm 2006-01-10 Attrib.rule;
2005-12-31 wenzelm 2005-12-31 elim rules: Classical.classical_rule;
2005-12-23 paulson 2005-12-23 the "skolem" attribute and better initialization of the clause database
2005-12-14 paulson 2005-12-14 removed unused function repeat_RS
2005-11-28 mengj 2005-11-28 Added two functions for CNF translation, used by other files.
2005-11-18 mengj 2005-11-18 -- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
2005-11-10 paulson 2005-11-10 duplicate axioms in ATP linkup, and general fixes
2005-11-09 paulson 2005-11-09 Skolemization by inference, but not quite finished
2005-10-28 paulson 2005-10-28 got rid of obsolete prove_goalw_cterm
2005-10-28 mengj 2005-10-28 Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names. Also added function "repeat_RS" to the signature.
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-10-19 mengj 2005-10-19 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
2005-10-11 paulson 2005-10-11 simplifying the treatment of clausification
2005-10-10 paulson 2005-10-10 small tidy-up of utility functions
2005-09-19 paulson 2005-09-19 simplification of the Isabelle-ATP code; hooks for batch generation of problems