src/Pure/Syntax/ROOT.ML
1997-02-28 wenzelm 1997-02-28 added token_trans.ML;
1996-12-10 wenzelm 1996-12-10 *** empty log message ***
1996-11-18 wenzelm 1996-11-18 added symbol_font.ML;
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-04-28 nipkow 1995-04-28 Added functor f() = struct end to hide functors to save space.
1994-08-19 wenzelm 1994-08-19 replaced SExtension by SynTrans (mixfix stuff in Mixfix); private structs now hidden within PrivateSyntax;
1994-06-09 wenzelm 1994-06-09 new datatype 'mixfix' now pervasive (old one still accesible via OldMixfix);
1994-05-19 wenzelm 1994-05-19 *** empty log message ***
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 minor internal changes;
1994-01-19 wenzelm 1994-01-19 minor internal changes;
1993-11-29 wenzelm 1993-11-29 added Scanner;
1993-10-11 wenzelm 1993-10-11 *** empty log message ***
1993-10-08 wenzelm 1993-10-08 *** 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