src/Pure/sorts.ML
2016-03-08 haftmann 2016-03-08 provide explicit hint concering uniqueness of derivation
2015-09-25 wenzelm 2015-09-25 tuned;
2015-09-25 wenzelm 2015-09-25 tuned signature: eliminated pointless type Context.pretty;
2012-07-16 wenzelm 2012-07-16 more direct Sorts.has_instance; tuned Sorts.mg_domain;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2012-02-23 wenzelm 2012-02-23 clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
2011-11-20 wenzelm 2011-11-20 clarified certify vs. sharing;
2011-08-20 wenzelm 2011-08-20 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-07-13 wenzelm 2011-07-13 Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one; Sorts.certify_class: prefer the persistent name;
2011-04-18 wenzelm 2011-04-18 pass plain Proof.context for pretty printing;
2011-04-18 wenzelm 2011-04-18 simplified Sorts.class_error: plain Proof.context; tuned;
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-09-24 wenzelm 2010-09-24 modernized structure Ord_List;
2010-09-01 haftmann 2010-09-01 replaced Table.map' by Table.map
2010-06-01 wenzelm 2010-06-01 arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML; misc tuning;
2010-04-27 wenzelm 2010-04-27 monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
2010-04-25 wenzelm 2010-04-25 replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-04-11 wenzelm 2010-04-11 modernized datatype constructors;
2010-04-11 wenzelm 2010-04-11 of_sort_derivation: weaken bypasses derivation for identical sort -- accomodate proof terms by krauss/schropp, for example;
2010-04-11 wenzelm 2010-04-11 tuned;
2010-04-11 wenzelm 2010-04-11 of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
2010-03-26 wenzelm 2010-03-26 more efficient merge_algebra for important special cases -- tricky due to required completion if class algebra changes;
2010-03-25 wenzelm 2010-03-25 Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS); officially export weaken as Sorts.classrel_derivation; tuned comments;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-09-30 wenzelm 2009-09-30 removed dead code; Sorts.of_sort_derivation: removed unused pp;
2009-07-06 wenzelm 2009-07-06 witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-23 haftmann 2009-02-23 stripped classrels_of, instances_of
2009-02-22 haftmann 2009-02-22 handle NONE case in arity function properly
2009-02-22 haftmann 2009-02-22 subalgebra: drop arities if desired
2009-02-18 haftmann 2009-02-18 sort instances wrt. to class hierarchy
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-01 haftmann 2008-12-01 more means for algebra projection
2008-10-22 haftmann 2008-10-22 added meet_sort_typ
2008-10-16 wenzelm 2008-10-16 added make, minimal_sorts;
2008-09-26 wenzelm 2008-09-26 added subset operation;
2008-09-25 wenzelm 2008-09-25 explicit type OrdList.T;
2008-07-11 wenzelm 2008-07-11 Sorts.weaken: abstract argument; tuned;
2008-07-11 haftmann 2008-07-11 fixed layout
2008-07-08 haftmann 2008-07-08 exported weaken combinator
2008-05-26 haftmann 2008-05-26 proper NoSubsort CLASS_ERROR
2008-04-13 wenzelm 2008-04-13 removed unused minimal_classes; class_error: produce message only (formerly msg_class_error); tuned;
2008-04-02 haftmann 2008-04-02 canonical meet_sort operation
2008-03-19 haftmann 2008-03-19 new class error case NoSubsort
2007-09-26 wenzelm 2007-09-26 added minimize_sort, complete_sort;
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-05 wenzelm 2007-07-05 sort_le: tuned eq case;
2007-04-03 wenzelm 2007-04-03 renamed of_sort_derivation record fields (avoid clash with Alice keywords);
2007-02-26 wenzelm 2007-02-26 removed obsolete eq_set;
2007-01-26 haftmann 2007-01-26 exported interface for explicit error messages
2007-01-25 haftmann 2007-01-25 added explicit query function for arities to subalgebra projection
2006-12-29 wenzelm 2006-12-29 classes: more direct way to achieve topological sorting; renamed classes to all_classes; added minimal_classes; renamed project to subalgebra, tuned;
2006-12-29 haftmann 2006-12-29 ``classes`` now returns classes in topological order
2006-09-18 wenzelm 2006-09-18 classes: maintain serial number;
2006-09-04 haftmann 2006-09-04 proper project_sort
2006-09-01 haftmann 2006-09-01 project_algebra yields sort projector
2006-08-17 haftmann 2006-08-17 added all_super_classes
2006-07-03 wenzelm 2006-07-03 project_algebra: norm_sort; tuned;