2007-08-09 ago new access interface in defs.ML
2007-08-03 ago replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-07-08 ago replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-05 ago removed comments -- no exception TERM;
2007-05-24 ago tuned Pure/General/name_space.ML
2007-05-07 ago simplified DataFun interfaces;
2007-04-15 ago removed obsolete inferT_axm;
2007-04-14 ago simplified read_axm;
2007-04-14 ago tuned signature;
2007-04-04 ago removed unused dep_graph;
2007-04-04 ago removed obsolete sign_of/sign_of_thm;
2007-03-20 ago added theory dependency graph
2006-12-11 ago advanced translation functions: Proof.context;
2006-11-30 ago added merge_list;
2006-09-15 ago removed type aliases for theory/theory_ref;
2006-08-17 ago dropped definitions_of
2006-07-19 ago Sign.infer_types: Name.context;
2006-06-07 ago renamed Type.(un)varifyT to Logic.(un)varifyT;
2006-05-25 ago tuned;
2006-05-24 ago added add_deps, which actually records dependencies of consts (unlike add_finals);
2006-05-22 ago Defs.specifications_of: lhs/rhs now use typargs;
2006-05-20 ago tuned Defs interfaces;
2006-05-13 ago Theory.add_defs(_i): added unchecked flag;
2006-05-11 ago tuned Defs.merge;
2006-05-08 ago Defs.define: const_typargs;
2006-05-05 ago added definitions_of;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-13 ago tuned;
2006-02-25 ago added more detailed data to consts
2006-02-07 ago adapted Sign.infer_types(_simult), Sign.certify_term/prop;
2006-02-06 ago moved no_vars to sign.ML;
2006-01-31 ago advanced translations: Context.generic;
2006-01-24 ago add_finals: prep_consts, i.e. varify type;
2006-01-14 ago sane ERROR handling;
2005-12-02 ago defs: beta/eta contract lhs;
2005-11-09 ago tuned;
2005-09-29 ago back to simple 'defs' (cf. revision 1.79);
2005-09-20 ago slight adaptions to library changes
2005-08-09 ago exported dest_def
2005-08-01 ago Compress.term;
2005-07-28 ago check_overloading replaces datatype overloading;
2005-07-19 ago tuned defs interface;
2005-07-13 ago tuned;
2005-07-07 ago 1) all theorems in Orderings can now be given as a parameter
2005-06-29 ago thy;
2005-06-22 ago renamed init to init_data;
2005-06-20 ago added begin_theory, end_theory;
2005-06-17 ago type theory, theory_ref, exception THEORY and related operations imported from Context;
2005-06-11 ago renamed hide_classes/types/consts to hide_XXX_i;
2005-06-09 ago axioms and oracles: NameSpace.table;
2005-06-07 ago A flag DEFS_CHAIN_HISTORY can be used to improve the error message
2005-06-05 ago renamed const_deps to defs;
2005-06-03 ago Integrates cycle detection in definitions with finalconsts
2005-06-02 ago Sign.restore_naming;
2005-05-31 ago Removed final_consts from theory data. Now const_deps deals with final
2005-05-31 ago added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
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).
2005-04-16 ago added del_modesyntax(_i);