wenzelm [Tue, 25 Jul 2006 21:18:08 +0200] rev 20201
added find_free (from term.ML);
wenzelm [Tue, 25 Jul 2006 21:18:07 +0200] rev 20200
added is/to_ascii_lower/upper;
tuned alphanum -- needs more work;
wenzelm [Tue, 25 Jul 2006 21:18:06 +0200] rev 20199
is_funtype: do not export internal operation;
added add_varnames (cf. add_vars etc.);
removed obsolete (add_)term_varnames;
removed find_free (moved to Isar/obtain.ML);
moved variant_abs to structure Syntax -- this is a syntax operation after all;
wenzelm [Tue, 25 Jul 2006 21:18:05 +0200] rev 20198
tuned;
wenzelm [Tue, 25 Jul 2006 21:18:04 +0200] rev 20197
use Term.add_vars instead of obsolete term_varnames;
wenzelm [Tue, 25 Jul 2006 21:18:02 +0200] rev 20196
renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);
wenzelm [Tue, 25 Jul 2006 21:18:01 +0200] rev 20195
tuned ML code;
wenzelm [Tue, 25 Jul 2006 21:18:00 +0200] rev 20194
renamed Term.variant_abs to Syntax.variant_abs;
wenzelm [Tue, 25 Jul 2006 21:17:58 +0200] rev 20193
Drule.merge_rules;
haftmann [Tue, 25 Jul 2006 16:51:26 +0200] rev 20192
renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum