src/Pure/defs.ML
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2009-11-16 ago tuned signature;
2009-11-15 ago primitive defs: clarified def (axiom name) vs. description;
2009-09-30 ago eliminated redundant parameters;
2009-07-18 ago tuned;
2009-07-17 ago tuned/modernized Envir.subst_XXX;
2009-01-21 ago removed Ids;
2007-10-01 ago tuned message;
2007-08-09 ago new access interface in defs.ML
2006-09-21 ago tuned;
2006-08-17 ago renamed module to thyname
2006-06-07 ago renamed Type.(un)varifyT to Logic.(un)varifyT;
2006-06-02 ago merge: always normalize (and check!) reductions;
2006-05-26 ago separate checks for acyclic/wellformed;
2006-05-25 ago tuned;
2006-05-24 ago made smlnj happy;
2006-05-24 ago wellformed: be less ambitious about structural containment;
2006-05-24 ago tuned;
2006-05-23 ago export plain_args;
2006-05-22 ago specifications_of: lhs/rhs represented as typargs;
2006-05-20 ago made smlnj happy;
2006-05-20 ago yet another re-implementation:
2006-05-13 ago actually reject malformed defs;
2006-05-12 ago tuned;
2006-05-12 ago improved propagate_deps;
2006-05-11 ago allow dependencies of disjoint collections of instances;
2006-05-08 ago simple substructure test for typargs (independent type constructors);
2006-05-05 ago specifications_of: more detailed information;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-06 ago exported specification names
2006-02-25 ago added more detailed data to consts
2006-02-15 ago specifications_of: avoid partiality;
2006-02-15 ago exported specifications_of
2006-02-12 ago simplified TableFun.join;
2005-10-27 ago removed inappropriate monomorphic test;
2005-10-08 ago more efficient check_specified, much less invocations;
2005-09-29 ago make signature constraint actually work;
2005-09-29 ago activate signature constraints;
2005-09-29 ago back to simple 'defs' (cf. revision 1.79 of theory.ML);
2005-09-27 ago corrected spelling bug
2005-09-27 ago added defs disclaimer
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-01 ago curried_lookup/update;
2005-08-01 ago chain_history: turned into runtime flag;
2005-07-28 ago Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;
2005-07-19 ago tuned interfaces declare, define, finalize, merge:
2005-07-14 ago use existing Inttab;
2005-07-14 ago - fixed bug concerning the renaming of axiom names
2005-07-11 ago Improved implementation of Defs.is_overloaded.
2005-07-07 ago 1) all theorems in Orderings can now be given as a parameter
2005-06-13 ago internalize axiom names in Defs.define; compress types via Term.compress_type
2005-06-11 ago further optimizations of cycle test
2005-06-07 ago 1) Fixed bug in Defs.merge_edges_1.
2005-06-03 ago Integrates cycle detection in definitions with finalconsts
2005-06-01 ago Preliminary version of defs.ML that does not check final consts.
2005-05-31 ago Removed final_consts from theory data. Now const_deps deals with final
2005-05-30 ago Infinite chains in definitions are now detected, too.
2005-05-29 ago Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).