2006-02-12 wenzelm 2006-02-12 simplified TableFun.join;
2005-10-27 wenzelm 2005-10-27 removed inappropriate monomorphic test;
2005-10-08 wenzelm 2005-10-08 more efficient check_specified, much less invocations; Type.could_unify filter;
2005-09-29 wenzelm 2005-09-29 make signature constraint actually work;
2005-09-29 wenzelm 2005-09-29 activate signature constraints;
2005-09-29 wenzelm 2005-09-29 back to simple 'defs' (cf. revision 1.79 of theory.ML); renamed 'finals' to 'specified', share bookkeeping with defs; added monomorphic;
2005-09-27 obua 2005-09-27 corrected spelling bug
2005-09-27 obua 2005-09-27 added defs disclaimer
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update; tuned;
2005-08-01 wenzelm 2005-08-01 chain_history: turned into runtime flag; added monomorphic; removed (inefficient) fast_overloading_info; Compress.typ; tuned;
2005-07-28 wenzelm 2005-07-28 Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;
2005-07-19 wenzelm 2005-07-19 tuned interfaces declare, define, finalize, merge: canonical argument order, produce errors; tuned checkT';
2005-07-14 wenzelm 2005-07-14 use existing Inttab;
2005-07-14 obua 2005-07-14 - fixed bug concerning the renaming of axiom names - introduced new function Defs.fast_overloading_info
2005-07-11 obua 2005-07-11 Improved implementation of Defs.is_overloaded.
2005-07-07 obua 2005-07-07 1) all theorems in Orderings can now be given as a parameter 2) new function Theory.defs_of 3) new functions Defs.overloading_info and Defs.is_overloaded
2005-06-13 obua 2005-06-13 internalize axiom names in Defs.define; compress types via Term.compress_type
2005-06-11 obua 2005-06-11 further optimizations of cycle test
2005-06-07 obua 2005-06-07 1) Fixed bug in Defs.merge_edges_1. 2) Major optimization of Defs.define: do not store dependencies between constants that cannot introduce cycles anyway. In that way, the cycle test adds almost no overhead to theories that define their constants in HOL-light / HOL4 style. 3) Cleaned up Defs.graph, no superfluous name tags are stored anymore.
2005-06-03 obua 2005-06-03 Integrates cycle detection in definitions with finalconsts
2005-06-01 obua 2005-06-01 Preliminary version of defs.ML that does not check final consts.
2005-05-31 obua 2005-05-31 Removed final_consts from theory data. Now const_deps deals with final constants.
2005-05-30 obua 2005-05-30 Infinite chains in definitions are now detected, too.
2005-05-29 obua 2005-05-29 Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).