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