src/Pure/Syntax/mixfix.ML
2016-03-29 wenzelm 2016-03-29 tuned messages -- more positions;
2016-03-29 wenzelm 2016-03-29 more position information for type mixfix;
2015-03-29 wenzelm 2015-03-29 tuned signature;
2014-02-26 wenzelm 2014-02-26 tuned signature;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2011-04-08 wenzelm 2011-04-08 more accurate markup for syntax consts, notably binders which point back to the original logical entity; tuned;
2011-04-08 wenzelm 2011-04-08 discontinued Syntax.max_pri, which is not really a symbolic parameter;
2011-04-08 wenzelm 2011-04-08 renamed sprop "prop#" to "prop'" -- proper identifier; eliminated spurious symbolic string bindings (logic, any etc.); hardwired special "prop" vs. "prop'" conversion; tuned;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext); clarified Syntax.root;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-07 wenzelm 2011-04-07 discontinued user-defined token translations; tuned signature;
2011-03-27 wenzelm 2011-03-27 removed unclear comments stemming from ed24ba6f69aa;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-03-01 wenzelm 2010-03-01 more uniform treatment of syntax for types vs. consts;
2010-02-26 wenzelm 2010-02-26 use simplified Syntax.escape;
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-15 wenzelm 2010-02-15 renamed InfixName to Infix etc.;
2010-02-15 wenzelm 2010-02-15 discontinued unnamed infix syntax;
2009-09-30 wenzelm 2009-09-30 eliminated dead code;
2009-03-07 wenzelm 2009-03-07 canonical argument order for type_name, const_name;
2009-01-19 wenzelm 2009-01-19 removed Ids;
2008-03-15 wenzelm 2008-03-15 tuned messages;
2007-10-17 wenzelm 2007-10-17 removed obsolete unlocalize_mixfix;
2007-04-30 wenzelm 2007-04-30 explicit treatment of legacy_features;
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;