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).