2015-08-10 wenzelm [Mon, 10 Aug 2015 13:54:12 +0200] rev 60873
tuned imports;
src/Tools/jEdit/src/documentation_dockable.scala

2015-08-10 wenzelm [Mon, 10 Aug 2015 11:23:49 +0200] rev 60872
tuned messages;
src/Pure/ML/ml_compiler_polyml.ML

2015-08-10 wenzelm [Mon, 10 Aug 2015 11:20:16 +0200] rev 60871
clarified ML options;
src/Pure/Tools/debugger.ML

2015-08-08 wenzelm [Sat, 08 Aug 2015 22:08:43 +0200] rev 60870
merged

2015-08-08 wenzelm [Sat, 08 Aug 2015 21:33:11 +0200] rev 60869
more single stepping;
src/Pure/Tools/debugger.ML src/Pure/Tools/debugger.scala src/Tools/jEdit/src/debugger_dockable.scala

2015-08-08 haftmann [Sat, 08 Aug 2015 10:51:33 +0200] rev 60868
direct bootstrap of integer division from natural division
NEWS src/HOL/Code_Numeral.thy src/HOL/Divides.thy src/HOL/Int.thy src/HOL/Library/Code_Binary_Nat.thy src/HOL/Library/Code_Target_Int.thy src/HOL/Library/Code_Target_Numeral.thy src/HOL/Library/Float.thy src/HOL/Library/Old_SMT/old_z3_proof_tools.ML src/HOL/Matrix_LP/ComputeNumeral.thy src/HOL/Tools/SMT/z3_replay_util.ML src/HOL/ex/Simproc_Tests.thy

2015-08-06 haftmann [Thu, 06 Aug 2015 23:56:48 +0200] rev 60867
slight cleanup of lemmas
src/HOL/Divides.thy src/HOL/Library/Formal_Power_Series.thy src/HOL/Library/Poly_Deriv.thy src/HOL/Library/Sum_of_Squares/sum_of_squares.ML src/HOL/Multivariate_Analysis/Integration.thy src/HOL/NSA/HyperDef.thy src/HOL/NSA/NSComplex.thy src/HOL/NSA/StarDef.thy src/HOL/NthRoot.thy src/HOL/Parity.thy src/HOL/Power.thy src/HOL/Rings.thy src/HOL/Series.thy src/HOL/Transcendental.thy src/HOL/Word/Bit_Representation.thy

2015-08-06 haftmann [Thu, 06 Aug 2015 19:12:09 +0200] rev 60866
obsolete since no code generator without dictionary construction left
src/HOL/Power.thy

2015-08-07 wenzelm [Fri, 07 Aug 2015 17:58:12 +0200] rev 60865
make SML/NJ work;
src/Pure/ML/exn_properties_dummy.ML

2015-08-07 wenzelm [Fri, 07 Aug 2015 16:15:53 +0200] rev 60864
suppress empty messages as usual;
src/Pure/Tools/debugger.ML