wenzelm [Sat, 24 Nov 2001 17:00:35 +0100] rev 12291
type variables: clarified "used" vs. "occ";
wenzelm [Sat, 24 Nov 2001 16:59:44 +0100] rev 12290
Library.gen_merge_lists';
wenzelm [Sat, 24 Nov 2001 16:59:32 +0100] rev 12289
clarified locale operations (rename, merge);
tuned;
wenzelm [Sat, 24 Nov 2001 16:58:57 +0100] rev 12288
print_locale: expr;
wenzelm [Sat, 24 Nov 2001 16:58:31 +0100] rev 12287
added join, merge_multi(');
tuned extend, make, merge;
wenzelm [Sat, 24 Nov 2001 16:57:34 +0100] rev 12286
merge_stamps: merge_lists' with reversed args;
wenzelm [Sat, 24 Nov 2001 16:56:26 +0100] rev 12285
gen_merge_lists;
wenzelm [Sat, 24 Nov 2001 16:55:56 +0100] rev 12284
added gen_merge_lists(') and merge_lists(');
removed obsolete generic_extend, generic_merge, extend_list;
wenzelm [Sat, 24 Nov 2001 16:55:00 +0100] rev 12283
gen_merge_lists';
wenzelm [Sat, 24 Nov 2001 16:54:32 +0100] rev 12282
generic_merge;