src/HOL/Library/LaTeXsugar.thy
21 months ago wenzelm 2018-01-25 clarified signature: items with \isasep are special;
21 months ago wenzelm 2018-01-18 clarified access to antiquotation options; define explicit variants of antiquotations; output proper Latex.text; misc tuning and clarification;
21 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
21 months ago wenzelm 2018-01-09 clarified modules;
2017-08-28 nipkow 2017-08-28 added eta_expansion and its documentation.
2016-09-22 wenzelm 2016-09-22 raw control symbols are superseded by Latex.embed_raw;
2016-07-08 nipkow 2016-07-08 new style dummy_pats
2016-05-23 wenzelm 2016-05-23 embedded content may be delimited via cartouches;
2016-03-05 wenzelm 2016-03-05 abbreviations for \<nexists>;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-05-16 nipkow 2014-05-16 new syntax for card, normalized spacing for #
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-09 wenzelm 2014-03-09 tuned signature;
2014-03-06 wenzelm 2014-03-06 eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
2014-03-06 wenzelm 2014-03-06 more uniform check_const/read_const;
2014-01-22 wenzelm 2014-01-22 merged
2014-01-22 wenzelm 2014-01-22 tuned signature;
2014-01-20 blanchet 2014-01-20 fixed typo
2012-09-28 nipkow 2012-09-28 new antiquotation const_typ
2011-02-13 nipkow 2011-02-13 more pretty set comprehension sugar
2010-02-21 wenzelm 2010-02-21 modernized notation -- to make it work for authentic syntax;
2009-06-05 haftmann 2009-06-05 Set.insert with authentic syntax
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-03-05 haftmann 2009-03-05 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-01-15 haftmann 2009-01-15 dropped $Id$
2008-07-28 nipkow 2008-07-28 *** empty log message ***
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2007-12-10 haftmann 2007-12-10 switched import from Main to List
2007-11-26 nipkow 2007-11-26 Removed forced roman font in mode=IfThen.
2007-02-16 schirmer 2007-02-16 added print-mode Axiom to print theorems without premises with a rule on top.
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-05-17 wenzelm 2006-05-17 const_syntax;
2005-05-30 nipkow 2005-05-30 added \nexists
2005-04-10 nipkow 2005-04-10 tuned
2005-01-27 nipkow 2005-01-27 fixed bugs
2005-01-26 nipkow 2005-01-26 new