src/Tools/subtyping.ML
2011-09-29 traytel 2011-09-29 correct coercion generation in case of unknown map functions
2011-08-17 traytel 2011-08-17 local coercion insertion algorithm to support complex coercions
2011-08-17 traytel 2011-08-17 printing and deleting of coercions
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-06-28 traytel 2011-06-28 collapse map functions with identity subcoercions to identities;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-04-19 wenzelm 2011-04-19 split Type_Infer into early and late part, after Proof_Context; added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;
2011-04-19 wenzelm 2011-04-19 simplified check/uncheck interfaces: result comparison is hardwired by default; tuned;
2011-04-18 wenzelm 2011-04-18 tuned signature;
2011-04-18 wenzelm 2011-04-18 standardized aliases of operations on tsig;
2011-04-18 wenzelm 2011-04-18 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;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2010-12-21 traytel 2010-12-21 Enabled non fully polymorphic map functions in subtyping
2010-12-03 wenzelm 2010-12-03 setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
2010-12-02 traytel 2010-12-02 use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
2010-12-01 wenzelm 2010-12-01 just one Term.dest_funT;
2010-12-01 wenzelm 2010-12-01 simplified equality on pairs of types;
2010-11-29 traytel 2010-11-29 two-staged architecture for subtyping; improved error messages of subtyping (using the new architecture); bugfix: constraint graph consistency check after cycle elimination;
2010-11-02 traytel 2010-11-02 Attribute map_function -> coercion_map; tuned;
2010-10-29 wenzelm 2010-10-29 more sharing of operations, without aliases;
2010-10-29 wenzelm 2010-10-29 simplified data lookup;
2010-10-29 wenzelm 2010-10-29 export declarations by default, to allow other ML packages by-pass concrete syntax; proper Args parsing for attribute syntax (required for proper treatment of morphisms when declarations are moved between contexts); tuned;
2010-10-29 wenzelm 2010-10-29 proper signature constraint for ML structure; explicit theory setup, which is customary outside Pure; formal @{binding} instead of Binding.name;
2010-10-29 wenzelm 2010-10-29 proper header; tuned whitespace;
2010-10-29 wenzelm 2010-10-29 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).