2010-03-03 ago more systematic mark/unmark operations;
2010-02-21 ago slightly more abstract syntax mark/unmark operations;
2009-03-18 ago de-camelized Symbol_Pos;
2009-01-19 ago removed Ids;
2009-01-02 ago added numeral, which supercedes num, xnum, float;
2008-12-23 ago renamed terminal category "float" to "float_token", to avoid name
2008-11-29 ago New lexical item "float".
2008-09-29 ago report_token/parse_token: back to context-less version;
2008-09-29 ago;
2008-08-15 ago token_kind: add Space, Comment;
2008-08-09 ago pos_of_token: Position.T;
2008-08-09 ago datatype token: maintain range, tuned representation;
2008-08-07 ago improved position handling due to SymbolPos.T;
2008-06-10 ago removed obsolete read_idents;
2008-01-28 ago basic scanners: produce symbol list instead of imploded string;
2007-09-18 ago simplified type int (eliminated, integer);
2007-09-15 ago replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
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 #~