src/Pure/Syntax/mixfix.ML
2007-04-15 wenzelm 2007-04-15 removed obsolete TypeInfer.logicT -- use dummyT;
2007-04-15 wenzelm 2007-04-15 added mixfixT (from type_infer.ML);
2006-12-12 wenzelm 2006-12-12 simplified unlocalize_mixfix;
2006-11-26 wenzelm 2006-11-26 Binder: syntax const is determined by binder_name, not its syntax;
2006-10-07 wenzelm 2006-10-07 refined unlocalize_mixfix;
2006-09-29 wenzelm 2006-09-29 removed mixfix_content;
2006-05-17 wenzelm 2006-05-17 always preserve authentic consts -- removed Syntax.mixfix_const;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-25 wenzelm 2006-04-25 unlocalize_mixfix: fallback on NoSyn;
2006-04-08 wenzelm 2006-04-08 removed fix_mixfix; added const_mixfix, mixfix_const;
2006-03-14 wenzelm 2006-03-14 turned string_of_mixfix into pretty_mixfix;
2006-02-11 wenzelm 2006-02-11 replaced mixfix_conflict by mixfix_content;
2006-02-10 wenzelm 2006-02-10 added mixfix_conflict;
2006-01-19 wenzelm 2006-01-19 moved pure syntax to Syntax/syntax.ML and pure_thy.ML;
2006-01-13 wenzelm 2006-01-13 mixfix: added Structure;
2006-01-04 wenzelm 2006-01-04 added unlocalize_mixfix;
2005-12-02 wenzelm 2005-12-02 mixfix_args: 1 for binders; string_of_mixfix: proper output of binders;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop;
2005-10-07 wenzelm 2005-10-07 added syntax for _idtdummy, _idtypdummy; removed obsolete _K;
2005-09-06 wenzelm 2005-09-06 deprecated old-style infix declarations, which mix name and syntax;
2005-06-29 wenzelm 2005-06-29 accomodate advanced trfuns;
2005-04-16 wenzelm 2005-04-16 identify binder translations only once (admits remove);
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-12-18 schirmer 2004-12-18 Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for printing.
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-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic' and '=?=' syntax;
2004-05-29 wenzelm 2004-05-29 \<^bsub>/\<^esub> syntax: unbreakable block;
2004-05-01 wenzelm 2004-05-01 improved indexed syntax / implicit structures;
2004-04-23 wenzelm 2004-04-23 index syntax: support for general expressions (input only);
2004-04-22 wenzelm 2004-04-22 non_typed_tr';
2004-01-27 nipkow 2004-01-27 Reduced space for xsymbols output of [| |] ==> from 3 to 1
2002-01-30 wenzelm 2002-01-30 added literal;
2002-01-16 wenzelm 2002-01-16 GPLed;
2001-12-18 wenzelm 2001-12-18 improved mixfix_args;
2001-12-14 wenzelm 2001-12-14 removed special treatment of "_" in syntax (now covered by \<index> arg);
2001-11-11 wenzelm 2001-11-11 pure_syntax_output: "_meta_conjunction";
2001-11-09 wenzelm 2001-11-09 removed pure_sym_syntax; allow additional arguments in infixes (maximum priority);
2001-11-08 wenzelm 2001-11-08 proper syntax for structs;
2001-11-07 wenzelm 2001-11-07 syntax for structs;
2001-10-28 wenzelm 2001-10-28 fixed string_of_mixfix;
2001-10-24 wenzelm 2001-10-24 added string_of_mixfix;
2001-10-02 wenzelm 2001-10-02 support non-oriented infix;
2001-02-11 wenzelm 2001-02-11 added "xsymbols" syntax for "=?=";
2000-08-29 wenzelm 2000-08-29 added \<dots> syntax;
1999-09-04 wenzelm 1999-09-04 removed "_BIND" syntax;
1999-07-08 wenzelm 1999-07-08 aprop: ??id, ...;
1999-06-02 wenzelm 1999-06-02 "..." syntax;
1999-04-14 wenzelm 1999-04-14 fixed named type infixes (actual BUG!);
1998-12-11 oheimb 1998-12-11 added new print_mode "xsymbols" for extended symbol support (e.g. genuiely long arrows)
1998-10-20 wenzelm 1998-10-20 no open;
1998-08-10 wenzelm 1998-08-10 ??id syntax for text variables;
1998-06-20 wenzelm 1998-06-20 added fix_mixfix;
1998-05-13 wenzelm 1998-05-13 pure_nonterms;
1998-04-22 wenzelm 1998-04-22 added no_syn;
1998-03-09 wenzelm 1998-03-09 Symbol.explode;
1997-11-05 wenzelm 1997-11-05 added TYPE syntax; tuned;
1997-10-31 wenzelm 1997-10-31 added mixfix_args;
1997-10-10 wenzelm 1997-10-10 added longid syntax;