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.
1995-07-03 clasohm 1995-07-03 added cargs for curried function application
1995-06-12 clasohm 1995-06-12 fixed bug in mfix_to_xprod: lambda productions' lhs shouldn't be modified
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-02-27 wenzelm 1995-02-27 new in mixfix annotations: "' " (quote space) separates delimiters without adding extra white space for printing;
1995-01-18 clasohm 1995-01-18 added optional precedence for body of binder; removed call to infer_types from read_xrules
1994-12-14 wenzelm 1994-12-14 removed "logic1"; improved typ_to_nonterm;
1994-12-08 clasohm 1994-12-08 changed Pure's grammar and the way types are converted to nonterminals
1994-10-04 clasohm 1994-10-04 made major changes to grammar; added call of Type.infer_types to automatically eliminate ambiguities
1994-08-19 wenzelm 1994-08-19 removed idT, varT, tidT, tvarT (now in lexicon.ML); added syn_ext_const_names, syn_ext_trfuns;
1994-06-29 clasohm 1994-06-29 changed precedence of constrain to [4, 0], 3
1994-05-17 clasohm 1994-05-17 fixed a bug in syntax_error, added "Building new grammar" message; automatically generated nonterminals now start with "@"
1994-05-11 clasohm 1994-05-11 changed implode to ^
1994-05-11 clasohm 1994-05-11 moved 'filter is_xid' in syn_ext
1994-04-26 clasohm 1994-04-26 made a few cosmetic 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 contains remaining parts of xgram.ML and extension.ML; syn_ext replaces xgram and ext;