src/Pure/defs.ML
2015-09-24 wenzelm 2015-09-24 more explicit Defs.context: use proper name spaces as far as possible;
2015-09-24 wenzelm 2015-09-24 explicit indication of overloaded typedefs;
2015-09-22 wenzelm 2015-09-22 tuned signature;
2015-09-22 wenzelm 2015-09-22 tuned signature;
2015-09-22 wenzelm 2015-09-22 tuned output;
2015-09-22 wenzelm 2015-09-22 renamed Defs.node to Defs.item; clarified type Defs.item; clarified item_ord for printing;
2015-09-22 wenzelm 2015-09-22 HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;
2014-11-24 wenzelm 2014-11-24 removed odd remains of structural containment checks, which stem from an older approach (see also 3ad1b289f21b, 3ae3cc4b1eac, 423af2e013b8, bad13b32c0f3, ccd6de95f4a6); de-facto this alternative never occured in practice, but it can lead to non-termination of the check;
2014-07-05 wenzelm 2014-07-05 proper plain_args to ensure that multi-argument overloading cannot escape pattern restriction (despite more liberal structural containment before 3ae3cc4b1eac);
2014-03-11 wenzelm 2014-03-11 minor performance tuning via fast matching filter;
2014-02-17 wenzelm 2014-02-17 more informative error;
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';