2015-11-02 eberlm [Mon, 02 Nov 2015 16:17:09 +0100] rev 61552
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
CONTRIBUTORS src/HOL/Binomial.thy src/HOL/Complex.thy src/HOL/Deriv.thy src/HOL/Int.thy src/HOL/Library/Formal_Power_Series.thy src/HOL/Limits.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Uniform_Limit.thy src/HOL/Transcendental.thy

2015-11-02 blanchet [Mon, 02 Nov 2015 21:58:38 +0100] rev 61551
don't pollute local theory with needless names
NEWS src/HOL/BNF_Fixpoint_Base.thy src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML

2015-11-02 blanchet [Mon, 02 Nov 2015 21:49:49 +0100] rev 61550
allow selectors and discriminators with same name as type
NEWS src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

2015-11-02 blanchet [Mon, 02 Nov 2015 21:49:49 +0100] rev 61549
make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
src/HOL/Tools/ATP/atp_problem.ML

2015-11-02 wenzelm [Mon, 02 Nov 2015 20:11:16 +0100] rev 61548
merged
src/HOL/Isar_Examples/document/style.tex

2015-11-02 wenzelm [Mon, 02 Nov 2015 18:31:57 +0100] rev 61547
avoid premature flushing and thus flashing of text area;
src/Pure/PIDE/query_operation.scala

2015-11-02 wenzelm [Mon, 02 Nov 2015 18:30:25 +0100] rev 61546
tuned whitespace;
src/HOL/Library/Lattice_Algebras.thy

2015-11-02 wenzelm [Mon, 02 Nov 2015 18:09:14 +0100] rev 61545
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
src/Pure/PIDE/query_operation.scala

2015-11-02 wenzelm [Mon, 02 Nov 2015 16:03:03 +0100] rev 61544
redundant;
src/Tools/jEdit/src/jedit_editor.scala

2015-11-02 wenzelm [Mon, 02 Nov 2015 16:02:32 +0100] rev 61543
tuned whitespace;
src/HOL/Hahn_Banach/Hahn_Banach.thy