src/Tools/subtyping.ML
17 months ago wenzelm 2017-12-06 prefer control symbol antiquotations;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-29 wenzelm 2015-03-29 proper local Proof_Context.arity_sorts;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-03-31 wenzelm 2014-03-31 some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-06 wenzelm 2014-03-06 more uniform check_const/read_const;
2014-02-26 wenzelm 2014-02-26 tuned signature;
2014-02-03 wenzelm 2014-02-03 unused;
2014-02-03 wenzelm 2014-02-03 more formal markup;
2014-02-03 wenzelm 2014-02-03 clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead; fewer squiggles;
2014-02-03 wenzelm 2014-02-03 just error, not a failed attempt to raise an exception;
2014-02-03 wenzelm 2014-02-03 tuned whitespace;
2013-11-26 traytel 2013-11-26 made SML/NJ happier
2013-11-25 traytel 2013-11-25 possibility to fold coercion inference error messages; tuned;
2013-11-18 traytel 2013-11-18 show all involved subtyping constraints that cause coercion inference to fail
2013-09-11 wenzelm 2013-09-11 tuned signature;
2013-06-23 wenzelm 2013-06-23 tuned message -- more markup;
2013-03-05 traytel 2013-03-05 allow more general coercion maps; tuned;
2013-03-04 traytel 2013-03-04 tuned (extend datatype to inline option)
2013-03-01 traytel 2013-03-01 constants with coercion-invariant arguments (possibility to disable/reenable coercions under certain constants, necessary for the forthcoming logically unspecified control structures for case translations)
2013-02-22 traytel 2013-02-22 tuned error messages
2013-02-22 traytel 2013-02-22 apply unifying substitution before building the constraint graph
2012-09-29 wenzelm 2012-09-29 more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-09-25 wenzelm 2012-09-25 tuned;
2012-09-25 wenzelm 2012-09-25 added graph encode/decode operations; tuned signature;
2012-09-05 traytel 2012-09-05 more conservative rechecking of processed constraints in subtyping constraint simplification
2012-03-21 wenzelm 2012-03-21 prefer explicitly qualified exception List.Empty;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-02-25 wenzelm 2012-02-25 discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
2012-02-23 wenzelm 2012-02-23 clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
2011-12-17 traytel 2011-12-17 meaningful error message on failing merges of coercion tables
2011-11-09 wenzelm 2011-11-09 tuned signature; tuned;
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;