src/HOL/Tools/res_axioms.ML
2008-04-12 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-10 wenzelm tuned;
2008-04-07 paulson * 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-01-02 paulson testing for empty sort
2007-10-31 paulson Catch exceptions arising during the abstraction operation.
2007-10-30 paulson bugfixes concerning strange theorems
2007-10-12 paulson trying to make it run faster
2007-10-11 wenzelm replaced Sign.add_consts_authentic by Sign.declare_const;
2007-10-09 paulson context-based treatment of generalization; also handling TFrees in axiom clauses
2007-10-05 paulson filtering out some package theorems
2007-10-04 paulson combinator translation
2007-10-02 wenzelm skolem_cache: ignore internal theorems -- major speedup;
2007-09-30 wenzelm llabs/sko: removed Name.internal;
2007-09-30 wenzelm skofuns/absfuns: explicit markup as internal consts;
2007-09-27 paulson removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
2007-09-21 wenzelm proper signature constraint;
2007-09-18 paulson metis now available in PreList
2007-08-16 wenzelm proper signature for Meson;
2007-08-10 paulson removal of some refs
2007-08-03 wenzelm replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-07-29 wenzelm simplified ResAtpset via NamedThmsFun;
2007-07-05 wenzelm renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-06-12 wenzelm renamed Goal.prove_raw to Goal.prove_internal;
2007-05-09 wenzelm moved some Drule operations to Thm (see more_thm.ML);
2007-05-06 wenzelm simplified DataFun interfaces;
2007-04-19 paulson trying to make single-step proofs work better, especially if they contain
2007-04-18 paulson Fixes for proof reconstruction, especially involving abstractions and definitions
2007-04-15 wenzelm Thm.fold_terms;
2007-04-12 paulson Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)
2007-04-04 wenzelm rep_thm/cterm/ctyp: removed obsolete sign field;
2007-03-26 paulson Clause cache is now in theory data.
2007-03-19 paulson Removal of axiom names from the theorem cache
2007-02-26 wenzelm moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-22 paulson Improved handling of situation when theorem in cache disagrees with theorem supplied: new clauses
2007-01-31 haftmann dropped lemma duplicates in HOL.thy
2007-01-20 wenzelm Output.debug: non-strict;
2007-01-04 paulson improvements to proof reconstruction. Some files loaded in a different order
2006-12-22 paulson tidying the ATP communications
2006-12-14 wenzelm avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-04 wenzelm thm/prf: separate official name vs. additional tags;
2006-11-30 wenzelm Goal.norm/close_result;
2006-11-29 wenzelm simplified method setup;
2006-11-23 wenzelm prefer Proof.context over Context.generic;
2006-11-22 paulson Consolidation of code to "blacklist" unhelpful theorems, including record
2006-11-21 paulson New transformation of eliminatino rules: we simply replace the final conclusion variable by False
2006-11-10 paulson Improvement to classrel clauses: now outputs the minimum needed.
2006-11-08 wenzelm incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
2006-10-26 paulson Conversion to clause form now tolerates Boolean variables without looping.
2006-10-23 paulson meson method MUST NOT use all safe rules, only basic ones for the logical connectives.
2006-10-20 paulson Fixed the "exception Empty" bug in elim2Fol
2006-10-12 paulson abstraction is now turned OFF...
2006-10-11 paulson Abstraction re-use code now checks that the abstraction function can be used in the current
2006-10-09 wenzelm replaced Drule.clhs/crhs_of by Drule.lhs/rhs_of;
2006-10-06 paulson Refinements to abstraction. Seeding with combinators K, I and B.
2006-10-05 paulson improvements to abstraction, ensuring more re-use of abstraction functions
2006-09-30 mengj Removed ResHolClause.LAM2COMB exception.
2006-09-29 wenzelm Sign.add_consts_authentic;
2006-09-28 wenzelm ResAtpset.get_atpset;
2006-09-26 paulson Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
2006-09-19 wenzelm sko/abs: Name.internal prevents choking of print_theory;
less more (0) -100 -60 tip