src/HOL/Library/OptionalSugar.thy
2015-09-09 wenzelm 2015-09-09 eliminated \<Colon> from syntax of constraints;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-01-20 hoelzl 2014-01-20 spelling
2014-01-18 wenzelm 2014-01-18 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); removed pointless space: the second "_ \<Colon> _" should take precendence anyway;
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;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-02-21 wenzelm 2010-02-21 proper markup of const syntax;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2009-11-02 wenzelm 2009-11-02 modernized structure Simple_Syntax;
2009-10-08 haftmann 2009-10-08 new generalized concept for term styles
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-03-13 nipkow 2009-03-13 added comment
2009-03-13 nipkow 2009-03-13 hiding numeric coercions in LaTeX
2009-03-12 nipkow 2009-03-12 optional latex sugar
2009-03-10 wenzelm 2009-03-10 more robust treatment of (authentic) consts within translations;
2009-01-15 haftmann 2009-01-15 type constraints and sort intersection
2007-05-06 nipkow 2007-05-06 added "set" supression
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-05-17 wenzelm 2006-05-17 const_syntax;
2005-01-27 nipkow 2005-01-27 fixed bugs
2005-01-26 nipkow 2005-01-26 new