2001-09-01 wenzelm 2001-09-01 tuned;
2001-08-31 berghofe 2001-08-31 Made consts list operations a bit faster.
2000-11-12 wenzelm 2000-11-12 removed junk;
2000-07-16 wenzelm 2000-07-16 AST translation rules no longer require constant head on LHS;
2000-05-21 wenzelm 2000-05-21 added read_sort;
2000-04-17 wenzelm 2000-04-17 Pretty.chunks;
1999-10-27 oheimb 1999-10-27 symbols in (error) messages now consistently with single backslash
1999-07-16 wenzelm 1999-07-16 tuned dest_lexicon;
1999-03-09 wenzelm 1999-03-09 token translation: real;
1999-01-29 oheimb 1999-01-29 corrected output of symbols for several (probably not all) relevant functions moved print_mode to ROOT.ML
1998-10-20 wenzelm 1998-10-20 made SML/NJ happy;
1998-10-20 wenzelm 1998-10-20 no open; handle multiple trfuns; tuned; removed trfun_names; structure BasicSyntax;
1998-05-02 wenzelm 1998-05-02 added trfun_names;
1998-03-09 wenzelm 1998-03-09 adapted to symbols, scan;
1998-02-12 wenzelm 1998-02-12 export map_trrule;
1997-12-29 wenzelm 1997-12-29 removed distinct_fst_string;
1997-12-28 wenzelm 1997-12-28 renamed Symtab.null to Symtab.empty;
1997-11-05 wenzelm 1997-11-05 adapted extend_trfunsT;
1997-11-03 wenzelm 1997-11-03 tuned: distinct_fst_string;
1997-10-10 wenzelm 1997-10-10 constify: qualified is const;
1997-10-06 wenzelm 1997-10-06 added simple_str_of_sort;
1997-10-06 wenzelm 1997-10-06 added pretty_sort; tuned read_typ; tuned pretty_term; removed string_of_term, string_of_typ;
1997-09-29 wenzelm 1997-09-29 improved warning;
1997-07-18 wenzelm 1997-07-18 tuned warning; renamed |-> <-| <-> to Parse/PrintRule;
1997-04-04 wenzelm 1997-04-04 fixed diagnostic output of print modes;
1997-02-28 wenzelm 1997-02-28 improved err msg;
1997-02-28 wenzelm 1997-02-28 added token translation support;
1997-02-06 wenzelm 1997-02-06 adapted read_typ, simple_read_typ;
1997-01-13 wenzelm 1997-01-13 replaced unit refs by 'stamp';
1996-12-13 wenzelm 1996-12-13 added extend_trfunsT; removed test: prtabs_of; removed chartrans;
1996-12-10 wenzelm 1996-12-10 added chartrans; prmode: added 'inout' option;
1996-12-02 paulson 1996-12-02 Removal of needless occurrences of "op"
1996-11-18 wenzelm 1996-11-18 extend_const_gram now supports multiple disjoint printer tables;
1996-06-18 paulson 1996-06-18 Translation infixes <->, etc., no longer available at top-level
1996-03-15 berghofe 1996-03-15 Added some functions which allow redirection of Isabelle's output
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-26 wenzelm 1995-06-26 added extend_trrules_i;
1995-06-14 clasohm 1995-06-14 removed 'raw' productions from gram datatype; replaced mk_gram by add_prods; completely changed the generation of internal grammars to reuse existing ones in extend_gram
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-01-27 wenzelm 1995-01-27 improved read_xrules: patterns no longer read twice; tuned read_typ;
1995-01-27 clasohm 1995-01-27 moved ambiguity_level from sign.ML to Syntax/syntax.ML
1995-01-18 clasohm 1995-01-18 added optional precedence for body of binder; removed call to infer_types from read_xrules
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 added type xrule (from sextension.ML); removed old 'extend'; removed added syn_ext_const_names, syn_ext_trfuns (now in syn_ext.ML); various minor changes;
1994-05-19 wenzelm 1994-05-19 added incremental extension functions: extend_log_types, extend_type_gram, extend_const_gram, extend_consts, extend_trfuns, extend_trrules; replaced merge by merge_syntaxes; 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-02-03 wenzelm 1994-02-03 added simple_string_of_typ, simple_pprint_typ; various internal changes;
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-30 wenzelm 1993-11-30 *** empty log message ***
1993-11-30 wenzelm 1993-11-30 *** empty log message ***
1993-11-30 wenzelm 1993-11-30 *** empty log message ***
1993-11-29 wenzelm 1993-11-29 *** empty log message ***
1993-11-29 wenzelm 1993-11-29 added (partial) extend_tables; improved extend; fixed roots handling of extend and merge;
1993-11-25 wenzelm 1993-11-25 added Syntax.read_typ; Syntax.extend: added read_ty, removed def_sort argument;
1993-10-11 wenzelm 1993-10-11 *** empty log message ***
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;
1993-09-16 clasohm 1993-09-16 Initial revision