2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-10-09 wenzelm 2008-10-09 improved performance of skolem cache, due to parallel map; misc tuning, less verbosity;
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-09-03 wenzelm 2008-09-03 Sign.declare_const: Name.binding;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-06-13 wenzelm 2008-06-13 skolem_fact/thm: uniform numbering, even for singleton list; declare_skofuns: eliminated recovery via Clausify_failure -- should be sufficiently robust as is;
2008-06-12 wenzelm 2008-06-12 use regular error function;
2008-06-12 wenzelm 2008-06-12 export just one setup function; more antiquotations; to_nnf: import open, avoiding internal variables (bounds); ThmCache: added table of seen fact names; reorganized skolem_thm/skolem_fact/saturate_skolem_cache: maintain seen fact names, ensure idempotent operation for Theory.at_end; removed obsolete skolem attribute (NB: official fact name unavailable here);
2008-06-12 wenzelm 2008-06-12 ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context; eliminated obscure theory merge/transfer -- use explicit theory context instead;
2008-06-12 wenzelm 2008-06-12 declare_skofuns/skolem: canonical argument order; minor tuning;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-15 wenzelm 2008-04-15 Thm.forall_elim_var(s);
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref; replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-10 wenzelm 2008-04-10 tuned;
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-01-02 paulson 2008-01-02 testing for empty sort
2007-10-31 paulson 2007-10-31 Catch exceptions arising during the abstraction operation. Filter out theorems that are "too deep".
2007-10-30 paulson 2007-10-30 bugfixes concerning strange theorems
2007-10-12 paulson 2007-10-12 trying to make it run faster
2007-10-11 wenzelm 2007-10-11 replaced Sign.add_consts_authentic by Sign.declare_const;
2007-10-09 paulson 2007-10-09 context-based treatment of generalization; also handling TFrees in axiom clauses
2007-10-05 paulson 2007-10-05 filtering out some package theorems
2007-10-04 paulson 2007-10-04 combinator translation
2007-10-03 wenzelm 2007-10-03 skolem_cache: ignore internal theorems -- major speedup; skolem_cache_theorems_of: efficient folding of table; replaced get_axiom by Thm.get_axiom_i (avoids name space fishing);
2007-09-30 wenzelm 2007-09-30 llabs/sko: removed Name.internal;
2007-09-30 wenzelm 2007-09-30 skofuns/absfuns: explicit markup as internal consts;
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-09-21 wenzelm 2007-09-21 proper signature constraint; minor tuning;
2007-09-18 paulson 2007-09-18 metis now available in PreList
2007-08-17 wenzelm 2007-08-17 proper signature for Meson;
2007-08-10 paulson 2007-08-10 removal of some refs
2007-08-03 wenzelm 2007-08-03 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-07-29 wenzelm 2007-07-29 simplified ResAtpset via NamedThmsFun;
2007-07-05 wenzelm 2007-07-05 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac; simplified ObjectLogic.atomize;
2007-06-13 wenzelm 2007-06-13 renamed Goal.prove_raw to Goal.prove_internal;
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