wenzelm [Tue, 25 Jul 2006 21:18:12 +0200] rev 20204
avoid Term.is_funtype;
wenzelm [Tue, 25 Jul 2006 21:18:11 +0200] rev 20203
avoid structure Char;
wenzelm [Tue, 25 Jul 2006 21:18:09 +0200] rev 20202
added variant_abs (from term.ML);
tuned;
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;