src/Pure/defs.ML
2011-04-18 wenzelm 2011-04-18 pass plain Proof.context for pretty printing;
2011-04-18 wenzelm 2011-04-18 pass plain Proof.context for pretty printing;
2011-04-18 wenzelm 2011-04-18 simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2009-11-16 wenzelm 2009-11-16 tuned signature;
2009-11-15 wenzelm 2009-11-15 primitive defs: clarified def (axiom name) vs. description;
2009-09-30 wenzelm 2009-09-30 eliminated redundant parameters;
2009-07-18 wenzelm 2009-07-18 tuned;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir.subst_XXX;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2007-10-01 wenzelm 2007-10-01 tuned message;
2007-08-09 haftmann 2007-08-09 new access interface in defs.ML
2006-09-21 wenzelm 2006-09-21 tuned;
2006-08-17 haftmann 2006-08-17 renamed module to thyname
2006-06-07 wenzelm 2006-06-07 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
2006-06-02 wenzelm 2006-06-02 merge: always normalize (and check!) reductions;
2006-05-26 wenzelm 2006-05-26 separate checks for acyclic/wellformed;
2006-05-25 wenzelm 2006-05-25 tuned;
2006-05-24 wenzelm 2006-05-24 made smlnj happy;
2006-05-24 wenzelm 2006-05-24 wellformed: be less ambitious about structural containment; tuned;
2006-05-24 wenzelm 2006-05-24 tuned;
2006-05-23 wenzelm 2006-05-23 export plain_args; tuned wellformed, normalize;
2006-05-22 wenzelm 2006-05-22 specifications_of: lhs/rhs represented as typargs; export pretty_const; export dest; more precise checking of lhs patterns; more precise normalization; misc cleanup;
2006-05-20 wenzelm 2006-05-20 made smlnj happy;
2006-05-20 wenzelm 2006-05-20 yet another re-implementation: . maintain explicit mapping from unspecified to specified consts (no dependency graph, no termination check, but direct reduction of specifications); . more precise checking of LHS patterns -- specialized patterns (e.g. 'a => 'a instead of general 'a => 'b) impose global restrictions;
2006-05-13 wenzelm 2006-05-13 actually reject malformed defs; added unchecked flag; tuned;
2006-05-12 wenzelm 2006-05-12 tuned;
2006-05-12 wenzelm 2006-05-12 improved propagate_deps; removed structs_less, which is actually unsound in conjunction with interdependent overloaded consts;
2006-05-11 wenzelm 2006-05-11 allow dependencies of disjoint collections of instances; major cleanup;
2006-05-08 wenzelm 2006-05-08 simple substructure test for typargs (independent type constructors);
2006-05-05 wenzelm 2006-05-05 specifications_of: more detailed information; tuned;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-06 haftmann 2006-04-06 exported specification names
2006-02-25 haftmann 2006-02-25 added more detailed data to consts
2006-02-15 wenzelm 2006-02-15 specifications_of: avoid partiality;
2006-02-15 haftmann 2006-02-15 exported specifications_of
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.