src/Tools/subtyping.ML
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
Tue, 19 Apr 2011 20:47:02 +0200 wenzelm split Type_Infer into early and late part, after Proof_Context;
Tue, 19 Apr 2011 14:57:09 +0200 wenzelm simplified check/uncheck interfaces: result comparison is hardwired by default;
Mon, 18 Apr 2011 20:40:31 +0200 wenzelm tuned signature;
Mon, 18 Apr 2011 13:52:23 +0200 wenzelm standardized aliases of operations on tsig;
Mon, 18 Apr 2011 12:11:58 +0200 wenzelm tuned;
Mon, 18 Apr 2011 11:13:29 +0200 wenzelm simplified pretty printing context, which is only required for certain kernel operations;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Tue, 21 Dec 2010 01:12:14 +0100 traytel Enabled non fully polymorphic map functions in subtyping
Fri, 03 Dec 2010 17:59:13 +0100 wenzelm setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
Thu, 02 Dec 2010 21:48:36 +0100 traytel use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
Wed, 01 Dec 2010 13:09:08 +0100 wenzelm just one Term.dest_funT;
Wed, 01 Dec 2010 11:06:01 +0100 wenzelm simplified equality on pairs of types;
Mon, 29 Nov 2010 16:53:08 +0100 traytel two-staged architecture for subtyping;
Tue, 02 Nov 2010 12:37:12 +0100 traytel Attribute map_function -> coercion_map;
Fri, 29 Oct 2010 22:54:54 +0200 wenzelm more sharing of operations, without aliases;
Fri, 29 Oct 2010 22:22:36 +0200 wenzelm simplified data lookup;
Fri, 29 Oct 2010 22:19:27 +0200 wenzelm export declarations by default, to allow other ML packages by-pass concrete syntax;
Fri, 29 Oct 2010 22:07:48 +0200 wenzelm proper signature constraint for ML structure;
Fri, 29 Oct 2010 21:49:33 +0200 wenzelm proper header;
Fri, 29 Oct 2010 21:34:07 +0200 wenzelm Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
less more (0) tip