wenzelm [Mon, 01 Aug 2005 19:20:44 +0200] rev 16990
removed atless (use term_ord instead);
removed (inefficient) insert_aterm;
improved bound: nameless, avoid allocating new strings;
tuned sort_ord/typ_ord: dict_ord;
tuned abstract_over: SAME;
tuned add_term_vars/frees: OrdList.insert;
removed compress_type/compress_type (cf. compress.ML);
wenzelm [Mon, 01 Aug 2005 19:20:43 +0200] rev 16989
export MataSimplifier.inherit_bounds;
wenzelm [Mon, 01 Aug 2005 19:20:42 +0200] rev 16988
Compress.typ;
wenzelm [Mon, 01 Aug 2005 19:20:41 +0200] rev 16987
Compress.init_data;
wenzelm [Mon, 01 Aug 2005 19:20:40 +0200] rev 16986
nameless Term.bound;
wenzelm [Mon, 01 Aug 2005 19:20:39 +0200] rev 16985
improved bounds: nameless Term.bound, recover names for output;
wenzelm [Mon, 01 Aug 2005 19:20:38 +0200] rev 16984
tuned dict_ord;
wenzelm [Mon, 01 Aug 2005 19:20:37 +0200] rev 16983
replaced atless by term_ord;
wenzelm [Mon, 01 Aug 2005 19:20:36 +0200] rev 16982
chain_history: turned into runtime flag;
added monomorphic;
removed (inefficient) fast_overloading_info;
Compress.typ;
tuned;
wenzelm [Mon, 01 Aug 2005 19:20:35 +0200] rev 16981
compression of terms and types by sharing common subtrees;
wenzelm [Mon, 01 Aug 2005 19:20:34 +0200] rev 16980
added compress.ML;
wenzelm [Mon, 01 Aug 2005 19:20:33 +0200] rev 16979
Term.is_bound;
wenzelm [Mon, 01 Aug 2005 19:20:32 +0200] rev 16978
tuned signature;
wenzelm [Mon, 01 Aug 2005 19:20:31 +0200] rev 16977
no eq_commute;
wenzelm [Mon, 01 Aug 2005 19:20:30 +0200] rev 16976
Defs.monomorphic;
wenzelm [Mon, 01 Aug 2005 19:20:29 +0200] rev 16975
Sign.read_term;
wenzelm [Mon, 01 Aug 2005 19:20:28 +0200] rev 16974
more zcong_sym;
wenzelm [Mon, 01 Aug 2005 19:20:26 +0200] rev 16973
simprocs: Simplifier.inherit_bounds;
wenzelm [Mon, 01 Aug 2005 19:20:25 +0200] rev 16972
no eq_sym_conv;
tuned;
wenzelm [Mon, 01 Aug 2005 19:20:24 +0200] rev 16971
removed read_cterm;
tuned;
wenzelm [Mon, 01 Aug 2005 19:20:23 +0200] rev 16970
tuned msg;
wenzelm [Mon, 01 Aug 2005 19:20:22 +0200] rev 16969
PolyML.Compiler.printInAlphabeticalOrder := false;
wenzelm [Mon, 01 Aug 2005 19:20:21 +0200] rev 16968
polyml: use polyml-platform/version from Isabelle distribution;
removed DEFS_CHAIN_HISTORY;
wenzelm [Mon, 01 Aug 2005 14:40:21 +0200] rev 16967
obsolete;