src/Pure/Syntax/lexicon.ML
2007-04-14 wenzelm 2007-04-14 removed redundant string_of_vname (see term.ML);
2007-04-03 wenzelm 2007-04-03 avoid overloaded integer constants (accomodate Alice);
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-12 wenzelm 2006-12-12 read_xnum: return leading_zeros, radix;
2006-12-11 wenzelm 2006-12-11 xstr: disallow backslashes;
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-08-02 wenzelm 2006-08-02 renamed Syntax.indexname to Syntax.read_indexname; added read_int (not Int.fromString, which admits ~ syntax of ML);
2006-07-19 wenzelm 2006-07-19 export is_tid;
2006-07-11 wenzelm 2006-07-11 uniform treatment of num/xnum; read_xnum: proper handling of bin/hex;
2006-07-11 wenzelm 2006-07-11 tuned;
2006-07-11 kleing 2006-07-11 hex and binary numerals (contributed by Rafal Kolanski)
2006-06-17 wenzelm 2006-06-17 moved internal/skolem to term.ML;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-02-10 wenzelm 2006-02-10 added fixedN, constN;
2005-12-08 wenzelm 2005-12-08 removed Syntax.deskolem;
2005-11-16 wenzelm 2005-11-16 added deskolem;
2005-05-31 wenzelm 2005-05-31 moved is_ident to General/symbol.ML;
2005-05-17 wenzelm 2005-05-17 added read_variable: optional question mark on input; removed obsolete token_assoc; scan_indexname: improved treatment of \<^isub> and \<^isup>; read_var: more robust against bad input; tuned;
2005-05-16 paulson 2005-05-16 Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-18 berghofe 2005-01-18 indexname function now parses type variables as well; changed input type from string list to string.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-29 wenzelm 2004-05-29 Library.read_int; Output.output;
2004-05-21 wenzelm 2004-05-21 string_of_vname moved to term.ML;
2004-05-11 berghofe 2004-05-11 Eta-expanded function scan_comment to make SmlNJ happy.
2004-05-10 wenzelm 2004-05-10 support nested comments;
2004-04-26 wenzelm 2004-04-26 added is_ascii_identifier;
2003-02-07 nipkow 2003-02-07 Added (* ... *) comments in formulae.
2002-01-16 wenzelm 2002-01-16 GPLed;
2001-10-05 wenzelm 2001-10-05 added "num" token;
2000-07-13 wenzelm 2000-07-13 added read_xnum;
2000-07-13 wenzelm 2000-07-13 added internal, dest_internal;
1999-10-07 wenzelm 1999-10-07 read_idents;
1999-09-04 wenzelm 1999-09-04 removed binding;
1999-07-10 wenzelm 1999-07-10 more specific exn;
1998-11-16 wenzelm 1998-11-16 tuned usage of read;
1998-11-14 wenzelm 1998-11-14 added read_nat;
1998-09-21 paulson 1998-09-21 Unary minus is now #- and not #~
1998-08-10 wenzelm 1998-08-10 dest_binding, dest_skolem;
1998-08-06 wenzelm 1998-08-06 binding / skolem vars;
1998-07-02 wenzelm 1998-07-02 Symbol.beginning;
1998-05-18 wenzelm 1998-05-18 Symbol.stopper;
1998-05-13 wenzelm 1998-05-13 adapted to new Scan.fail_with / Scan.!!;
1998-05-07 wenzelm 1998-05-07 added scan_tvar;
1998-03-09 wenzelm 1998-03-09 adapted to symbols, scan;
1998-01-30 wenzelm 1998-01-30 added read_var;
1997-11-20 wenzelm 1997-11-20 added implode_xstr: string list -> string, explode_xstr: string -> string list;
1997-10-10 wenzelm 1997-10-10 added longid;
1997-02-06 wenzelm 1997-02-06 added string_of_vname' (treats neg. index as free);
1996-12-10 wenzelm 1996-12-10 tokenize: no gets exploded char list;
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1995-06-06 lcp 1995-06-06 Now string_of_vname checks for the empty variable name, catching the exception LIST.
1994-08-19 wenzelm 1994-08-19 replaced id, var, tid, tvar by idT, varT, tidT, tvarT; added const, free, var: build atomic terms of dummyT; added 'xnum' (signed numerals) and 'xstr' (strings) token kinds; various minor internal changes;
1994-05-18 wenzelm 1994-05-18 extended signature SCANNER by some basic scanners and type lexicon; various minor internal changes;
1994-04-22 clasohm 1994-04-22 changed the way a grammar is generated to allow the new parser to work; also made a lot of changes in parser.ML and minor ones elsewhere
1994-01-19 wenzelm 1994-01-19 MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables now much leaner (eliminated gramgraph, all data except tables of old parser are shared); simplified the internal interfaces for syntax extension;
1993-11-29 wenzelm 1993-11-29 added SCANNER; changed scan_any: no longer uses take_prefix;
1993-10-04 wenzelm 1993-10-04 lots of internal cleaning and tuning; removed {parse,print}_{pre,post}_proc; new lexer: now human readable due to scanner combinators; new parser installed, but still inactive (due to grammar ambiguities); added Syntax.test_read; typ_of_term: sorts now made distinct and sorted; mixfix: added forced line breaks (//); PROP now printed before subterm of type prop with non-const head;