tuned signature;

proper sort constraints for strip_shyps, for sort relations used in minimization;

export sort algebra;

provide explicit hint concering uniqueness of derivation

tuned;

tuned signature: eliminated pointless type Context.pretty;

more direct Sorts.has_instance;
tuned Sorts.mg_domain;

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;

clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;

clarified certify vs. sharing;

refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;

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;

pass plain Proof.context for pretty printing;

simplified Sorts.class_error: plain Proof.context;
tuned;

simplified pretty printing context, which is only required for certain kernel operations;
disentangled dependencies of structure Pretty;

modernized structure Ord_List;

replaced Table.map' by Table.map

arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML;
misc tuning;

monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;

replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;

modernized datatype constructors;

of_sort_derivation: weaken bypasses derivation for identical sort -- accomodate proof terms by krauss/schropp, for example;

tuned;

of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;

more efficient merge_algebra for important special cases -- tricky due to required completion if class algebra changes;

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;

modernized structure Term_Ord;

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

removed dead code;
Sorts.of_sort_derivation: removed unused pp;

witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;

Merge.

stripped classrels_of, instances_of

handle NONE case in arity function properly

subalgebra: drop arities if desired

sort instances wrt. to class hierarchy

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;

more means for algebra projection

added meet_sort_typ

added make, minimal_sorts;

added subset operation;

explicit type OrdList.T;

Sorts.weaken: abstract argument;
tuned;

fixed layout

exported weaken combinator

proper NoSubsort CLASS_ERROR

removed unused minimal_classes;
class_error: produce message only (formerly msg_class_error);
tuned;

canonical meet_sort operation

new class error case NoSubsort

added minimize_sort, complete_sort;

replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;

sort_le: tuned eq case;

renamed of_sort_derivation record fields (avoid clash with Alice keywords);

removed obsolete eq_set;

exported interface for explicit error messages

added explicit query function for arities to subalgebra projection

classes: more direct way to achieve topological sorting;
renamed classes to all_classes;
added minimal_classes;
renamed project to subalgebra, tuned;

``classes`` now returns classes in topological order

classes: maintain serial number;

proper project_sort

project_algebra yields sort projector

added all_super_classes

project_algebra: norm_sort;
tuned;

added class projection

abstract interfaces for type algebra;
tuned;

tuned;

added class_error and exception CLASS_ERROR (supercedes DOMAIN);
clarified of_class_derivation;
tuned witness_sorts;

tuned;

added domain_error;
added of_sort_derivation;
tuned;

arities: maintain original codomain;

moved certify_class/sort to type.ML;
added operations to build sort algebras (from type.ML);
tuned;

tuned basic list operators (flat, maps, map_filter);

added remove_sort;

removed superclasses (see sign.ML);

removed unused class_le_path, sort_less;

TableFun: renamed xxx_multi to xxx_list;

sort_distinct;

minor tweaks for Poplog/ML;

TableFun/Symtab: curried lookup and update;

curried_lookup/update;

use AList operations;

added superclasses, class_le_path

tuned norm_sort, mg_domain;

removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
added efficient operations on ordered lists: eq_set, union, subtract, insert_sort/typ(s)/term(s);

(undone experimental changes)

subclassing done

Move towards standard functions.

Deleted Library.option type.

added certify_class/sort;

tuned comments;

improved output; refer to Pretty.pp;

incorporate sort ops from term.ML; use Graph.T; misc cleanup;

inter_sort: keep normal!

mg_domain: exception DOMAIN;
proper witness_sorts;
removed nonempty_sort;

replace assoc lists by Symtab.table;

now uses Syntax.simple_str_of_sort;

added str_of_classrel;

removed least_sort;
added of_sort;

Type classes and sorts (isolated from type.ML).