2014-03-31 ago some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-06 ago more uniform check_const/read_const;
2014-02-26 ago tuned signature;
2014-02-03 ago unused;
2014-02-03 ago more formal markup;
2014-02-03 ago clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
2014-02-03 ago just error, not a failed attempt to raise an exception;
2014-02-03 ago tuned whitespace;
2013-11-26 ago made SML/NJ happier
2013-11-25 ago possibility to fold coercion inference error messages; tuned;
2013-11-18 ago show all involved subtyping constraints that cause coercion inference to fail
2013-09-11 ago tuned signature;
2013-06-23 ago tuned message -- more markup;
2013-03-05 ago allow more general coercion maps; tuned;
2013-03-04 ago tuned (extend datatype to inline option)
2013-03-01 ago constants with coercion-invariant arguments (possibility to disable/reenable
2013-02-22 ago tuned error messages
2013-02-22 ago apply unifying substitution before building the constraint graph
2012-09-29 ago more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-09-25 ago tuned;
2012-09-25 ago added graph encode/decode operations;
2012-09-05 ago more conservative rechecking of processed constraints in subtyping constraint simplification
2012-03-21 ago prefer explicitly qualified exception List.Empty;
2012-03-16 ago outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-02-25 ago discontinued slightly odd Graph.del_nodes (inefficient due to full;
2012-02-23 ago clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
2011-12-17 ago meaningful error message on failing merges of coercion tables
2011-11-09 ago tuned signature;
2011-09-29 ago correct coercion generation in case of unknown map functions
2011-08-17 ago local coercion insertion algorithm to support complex coercions
2011-08-17 ago printing and deleting of coercions
2011-08-20 ago refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-06-28 ago collapse map functions with identity subcoercions to identities;
2011-06-08 ago more robust exception pattern General.Subscript;
2011-05-02 ago added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
2011-04-19 ago split Type_Infer into early and late part, after Proof_Context;
2011-04-19 ago simplified check/uncheck interfaces: result comparison is hardwired by default;
2011-04-18 ago tuned signature;
2011-04-18 ago standardized aliases of operations on tsig;
2011-04-18 ago tuned;
2011-04-18 ago simplified pretty printing context, which is only required for certain kernel operations;
2011-04-16 ago modernized structure Proof_Context;
2011-04-08 ago explicit structure Syntax_Trans;
2010-12-21 ago Enabled non fully polymorphic map functions in subtyping
2010-12-03 ago setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
2010-12-02 ago use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
2010-12-01 ago just one Term.dest_funT;
2010-12-01 ago simplified equality on pairs of types;
2010-11-29 ago two-staged architecture for subtyping;
2010-11-02 ago Attribute map_function -> coercion_map;
2010-10-29 ago more sharing of operations, without aliases;
2010-10-29 ago simplified data lookup;
2010-10-29 ago export declarations by default, to allow other ML packages by-pass concrete syntax;
2010-10-29 ago proper signature constraint for ML structure;
2010-10-29 ago proper header;
2010-10-29 ago Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).