2015-11-03 wenzelm [Tue, 03 Nov 2015 16:35:00 +0100] rev 61558
tuned;
src/Pure/General/exn.scala src/Tools/jEdit/src/scala_console.scala

2015-11-03 wenzelm [Tue, 03 Nov 2015 14:03:44 +0100] rev 61557
prefer ad-hoc non-worker threads;
src/Tools/jEdit/src/active.scala src/Tools/jEdit/src/documentation_dockable.scala src/Tools/jEdit/src/jedit_editor.scala

2015-11-03 wenzelm [Tue, 03 Nov 2015 13:54:34 +0100] rev 61556
clarified modules;
Admin/polyml/future/ROOT.ML src/HOL/Tools/Sledgehammer/async_manager_legacy.ML src/Pure/Concurrent/bash.ML src/Pure/Concurrent/bash_windows.ML src/Pure/Concurrent/consumer_thread.scala src/Pure/Concurrent/event_timer.ML src/Pure/Concurrent/future.ML src/Pure/Concurrent/future.scala src/Pure/Concurrent/par_list.scala src/Pure/Concurrent/simple_thread.ML src/Pure/Concurrent/simple_thread.scala src/Pure/Concurrent/standard_thread.ML src/Pure/Concurrent/standard_thread.scala src/Pure/Concurrent/time_limit.ML src/Pure/GUI/gui_thread.scala src/Pure/PIDE/prover.scala src/Pure/PIDE/session.scala src/Pure/ROOT src/Pure/ROOT.ML src/Pure/System/invoke_scala.scala src/Pure/System/isabelle_system.scala src/Pure/System/message_channel.ML src/Pure/Tools/build.scala src/Pure/Tools/debugger.ML src/Pure/Tools/debugger.scala src/Pure/build-jars src/Tools/jEdit/src/pretty_text_area.scala src/Tools/jEdit/src/session_build.scala src/Tools/jEdit/src/text_overview.scala

2015-11-03 wenzelm [Tue, 03 Nov 2015 11:24:42 +0100] rev 61555
cancel already running request;
src/Pure/Concurrent/simple_thread.scala

2015-11-03 eberlm [Tue, 03 Nov 2015 15:24:24 +0100] rev 61554
added acknowledgement in Binomial.thy
src/HOL/Binomial.thy

2015-11-03 eberlm [Tue, 03 Nov 2015 11:20:21 +0100] rev 61553
Merged
src/HOL/Isar_Examples/document/style.tex

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