Sun, 16 Oct 2011 18:48:30 +0200 |
wenzelm |
added Term.dummy_pattern conveniences;
|
file |
diff |
annotate
|
Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
Wed, 06 Jul 2011 20:14:13 +0200 |
wenzelm |
tuned errors;
|
file |
diff |
annotate
|
Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
file |
diff |
annotate
|
Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
file |
diff |
annotate
|
Wed, 01 Dec 2010 15:03:44 +0100 |
wenzelm |
more direct use of binder_types/body_type;
|
file |
diff |
annotate
|
Wed, 01 Dec 2010 13:37:31 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 01 Dec 2010 13:09:08 +0100 |
wenzelm |
just one Term.dest_funT;
|
file |
diff |
annotate
|
Mon, 13 Sep 2010 00:10:29 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 02 Sep 2010 00:48:07 +0200 |
wenzelm |
turned show_question_marks into proper configuration option;
|
file |
diff |
annotate
|
Sat, 27 Mar 2010 15:47:57 +0100 |
wenzelm |
added Term.fold_atyps_sorts convenience;
|
file |
diff |
annotate
|
Fri, 19 Feb 2010 11:06:22 +0100 |
haftmann |
added dest_comb
|
file |
diff |
annotate
|
Thu, 28 Jan 2010 22:39:48 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 15 Nov 2009 15:14:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 09 Nov 2009 20:47:39 +0100 |
wenzelm |
locale_const/target_notation: uniform use of Term.aconv_untyped;
|
file |
diff |
annotate
|
Thu, 22 Oct 2009 13:48:06 +0200 |
haftmann |
map_range (and map_index) combinator
|
file |
diff |
annotate
|
Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
Sun, 26 Jul 2009 13:12:53 +0200 |
wenzelm |
lambda/cabs/all: named variants;
|
file |
diff |
annotate
|
Thu, 16 Jul 2009 21:00:09 +0200 |
wenzelm |
use structure Same;
|
file |
diff |
annotate
|
Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
Thu, 05 Mar 2009 17:09:07 +0100 |
wenzelm |
close_schematic_term: uniform order of types/terms;
|
file |
diff |
annotate
|
Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
Fri, 27 Feb 2009 16:38:52 +0100 |
wenzelm |
eliminated NJ's List.nth;
|
file |
diff |
annotate
|
Fri, 27 Feb 2009 16:18:02 +0100 |
wenzelm |
tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
|
file |
diff |
annotate
|