2013-01-31 blanchet [Thu, 31 Jan 2013 12:09:07 +0100] rev 51001
adapted to new MaSh interface
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

2013-01-31 hoelzl [Thu, 31 Jan 2013 11:31:30 +0100] rev 51000
use order topology for extended reals
src/HOL/Library/Extended_Nat.thy src/HOL/Library/Extended_Real.thy src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy src/HOL/Probability/Discrete_Topology.thy src/HOL/Probability/Lebesgue_Integration.thy src/HOL/Probability/Lebesgue_Measure.thy src/HOL/Probability/Measure_Space.thy src/HOL/Probability/Regularity.thy

2013-01-31 hoelzl [Thu, 31 Jan 2013 11:31:27 +0100] rev 50999
introduce order topology
src/HOL/Limits.thy src/HOL/RealVector.thy src/HOL/SEQ.thy src/HOL/Series.thy src/HOL/Set_Interval.thy

2013-01-31 hoelzl [Thu, 31 Jan 2013 11:31:22 +0100] rev 50998
simplify heine_borel type class
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

2013-01-31 blanchet [Thu, 31 Jan 2013 11:20:12 +0100] rev 50997
compute proper weight for "p proves p" in MaSh
src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py

2013-01-15 kuncar [Tue, 15 Jan 2013 12:13:27 +0100] rev 50996
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
src/HOL/Codegenerator_Test/RBT_Set_Test.thy src/HOL/Library/RBT_Set.thy

2013-01-25 nipkow [Fri, 25 Jan 2013 16:45:09 +0100] rev 50995
tuned
src/HOL/IMP/Abs_Int1_const.thy src/HOL/IMP/Abs_Int1_parity.thy src/HOL/IMP/Abs_Int2.thy src/HOL/IMP/Abs_Int2_ivl.thy src/HOL/IMP/Abs_Int3.thy src/HOL/IMP/Abs_State.thy

2013-01-20 wenzelm [Sun, 20 Jan 2013 15:34:27 +0100] rev 50994
back to post-release mode -- after fork point;
CONTRIBUTORS NEWS

2013-01-20 wenzelm [Sun, 20 Jan 2013 15:26:56 +0100] rev 50993
updated for release;
CONTRIBUTORS NEWS

2013-01-20 wenzelm [Sun, 20 Jan 2013 14:05:37 +0100] rev 50992
merged