Mon, 01 Aug 2005 19:20:42 +0200 | wenzelm | Compress.typ; | changeset | files |
Mon, 01 Aug 2005 19:20:41 +0200 | wenzelm | Compress.init_data; | changeset | files |
Mon, 01 Aug 2005 19:20:40 +0200 | wenzelm | nameless Term.bound; | changeset | files |
Mon, 01 Aug 2005 19:20:39 +0200 | wenzelm | improved bounds: nameless Term.bound, recover names for output; | changeset | files |
Mon, 01 Aug 2005 19:20:38 +0200 | wenzelm | tuned dict_ord; | changeset | files |
Mon, 01 Aug 2005 19:20:37 +0200 | wenzelm | replaced atless by term_ord; | changeset | files |