2007-08-13 ago Lexicon.tokenize: do not appen EndToken yet;
2007-07-12 ago sys_error;
2007-07-11 ago Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2007-04-14 ago removed redundant string_of_vname (see term.ML);
2007-04-03 ago avoid overloaded integer constants (accomodate Alice);
2006-12-15 ago avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-12 ago read_xnum: return leading_zeros, radix;
2006-12-11 ago xstr: disallow backslashes;
2006-09-21 ago member (op =);
2006-08-02 ago renamed Syntax.indexname to Syntax.read_indexname;
2006-07-19 ago export is_tid;
2006-07-11 ago uniform treatment of num/xnum;
2006-07-11 ago tuned;
2006-07-11 ago hex and binary numerals (contributed by Rafal Kolanski)
2006-06-17 ago moved internal/skolem to term.ML;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-03-21 ago avoid polymorphic equality;
2006-02-10 ago added fixedN, constN;
2005-12-08 ago removed Syntax.deskolem;
2005-11-16 ago added deskolem;
2005-05-31 ago moved is_ident to General/symbol.ML;
2005-05-17 ago added read_variable: optional question mark on input;
2005-05-16 ago Use of instead of int in most numeric simprocs; avoids
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2005-01-18 ago indexname function now parses type variables as well; changed input
2004-06-21 ago Merged in license change from Isabelle2004
2004-05-29 ago Library.read_int; Output.output;
2004-05-21 ago string_of_vname moved to term.ML;
2004-05-11 ago Eta-expanded function scan_comment to make SmlNJ happy.
2004-05-10 ago support nested comments;
2004-04-26 ago added is_ascii_identifier;
2003-02-07 ago Added (* ... *) comments in formulae.
2002-01-16 ago GPLed;
2001-10-05 ago added "num" token;
2000-07-13 ago added read_xnum;
2000-07-13 ago added internal, dest_internal;
1999-10-07 ago read_idents;
1999-09-04 ago removed binding;
1999-07-10 ago more specific exn;
1998-11-16 ago tuned usage of read;
1998-11-14 ago added read_nat;
1998-09-21 ago Unary minus is now #- and not #~
1998-08-10 ago dest_binding, dest_skolem;
1998-08-06 ago binding / skolem vars;
1998-07-02 ago Symbol.beginning;
1998-05-18 ago Symbol.stopper;
1998-05-13 ago adapted to new Scan.fail_with / Scan.!!;
1998-05-07 ago added scan_tvar;
1998-03-09 ago adapted to symbols, scan;
1998-01-30 ago added read_var;
1997-11-20 ago added implode_xstr: string list -> string, explode_xstr: string -> string list;
1997-10-10 ago added longid;
1997-02-06 ago added string_of_vname' (treats neg. index as free);
1996-12-10 ago tokenize: no gets exploded char list;
1996-02-16 ago Elimination of fully-functorial style.
1995-06-06 ago Now string_of_vname checks for the empty variable name,
1994-08-19 ago replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
1994-05-18 ago extended signature SCANNER by some basic scanners and type lexicon;
1994-04-22 ago changed the way a grammar is generated to allow the new parser to work;