src/Pure/Syntax/syn_ext.ML
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-09-30 wenzelm 2009-09-30 eliminated redundant parameters;
2009-03-01 wenzelm 2009-03-01 discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
2009-01-19 wenzelm 2009-01-19 removed Ids;
2009-01-02 wenzelm 2009-01-02 added numeral, which supercedes num, xnum, float; renamed xstr to inner_string;
2008-11-29 nipkow 2008-11-29 New lexical item "float".
2008-11-20 wenzelm 2008-11-20 Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-04-17 wenzelm 2008-04-17 token translations: context dependent, result Pretty.T; string_of_term/prop: Variable.auto_fixes;
2007-10-17 wenzelm 2007-10-17 removed obsolete unlocalize_mfix;
2007-07-11 wenzelm 2007-07-11 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2007-07-09 wenzelm 2007-07-09 type output = string indicates raw system output;
2007-07-07 wenzelm 2007-07-07 simplified pretty token metric: type int;
2007-04-03 wenzelm 2007-04-03 avoid clash with Alice keywords;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-11 wenzelm 2006-12-11 advanced translation functions: Proof.context;
2006-09-21 wenzelm 2006-09-21 member (op =); tuned;
2006-07-11 wenzelm 2006-07-11 Name.invent_list;
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-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-11 wenzelm 2006-02-11 tuned;
2006-02-10 wenzelm 2006-02-10 added mfix_delims; tuned;
2006-02-08 haftmann 2006-02-08 introduced gen_distinct in place of distinct
2006-01-31 wenzelm 2006-01-31 advanced translations: Context.generic;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-04 wenzelm 2006-01-04 added unlocalize_mfix;
2005-06-29 wenzelm 2005-06-29 accomodate advanced trfuns;
2005-05-17 wenzelm 2005-05-17 tuned;
2005-04-23 wenzelm 2005-04-23 added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);
2005-04-16 wenzelm 2005-04-16 added stamp_trfun, mk_trfun, eq_trfun;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-09 wenzelm 2004-06-09 removed separate logtypes field of syntax;
2004-05-29 wenzelm 2004-05-29 Library.read_int;
2004-05-01 wenzelm 2004-05-01 improved indexed syntax / implicit structures;
2004-04-22 wenzelm 2004-04-22 non_typed_tr';
2002-01-30 wenzelm 2002-01-30 escape_mfix;
2002-01-16 wenzelm 2002-01-16 GPLed;
2001-12-14 wenzelm 2001-12-14 support for ``indexed syntax'' (using "\<index>" argument instead of "_");
2001-09-01 wenzelm 2001-09-01 tuned;
2000-07-17 wenzelm 2000-07-17 consts: include *all* names;
1999-09-04 wenzelm 1999-09-04 removed binding;
1999-06-02 wenzelm 1999-06-02 added dddot_indexname;
1999-03-09 wenzelm 1999-03-09 token translation: real;
1998-11-16 wenzelm 1998-11-16 Scan.read;
1998-10-20 wenzelm 1998-10-20 no open;
1998-05-18 wenzelm 1998-05-18 Symbol.stopper;
1998-03-09 wenzelm 1998-03-09 adapted to new scanner and abroque chars;
1997-11-05 wenzelm 1997-11-05 adapted syn_ext_trfunsT;
1997-10-31 wenzelm 1997-10-31 tuned;
1997-10-30 wenzelm 1997-10-30 added mixfix_args;
1997-04-04 wenzelm 1997-04-04 fixed diagnostic output of print modes;
1997-02-28 wenzelm 1997-02-28 added token_translation interface;
1996-12-13 wenzelm 1996-12-13 added fix_tr', syn_ext_trfunsT; changed syn_ext_trfuns (fix_tr');
1996-12-10 wenzelm 1996-12-10 mfix_to_xprod: now uses read_charnames;
1996-11-27 wenzelm 1996-11-27 changed symbolic char syntax to \<NAME>
1996-11-19 wenzelm 1996-11-19 minor tuning;
1996-11-18 wenzelm 1996-11-18 new delimiter syntax in mixfixes: \{SYMBOLNAME} is char from symbol font;
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.