2014-05-30 nipkow [Fri, 30 May 2014 18:13:40 +0200] rev 57136
must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
src/HOL/Rat.thy src/HOL/Tools/numeral_simprocs.ML

2014-05-30 wenzelm [Fri, 30 May 2014 16:10:57 +0200] rev 57135
merged

2014-05-30 wenzelm [Fri, 30 May 2014 15:34:14 +0200] rev 57134
updated cygwin -- include perl_vendor for libwww-perl;
Admin/components/bundled-windows Admin/components/components.sha1 Admin/lib/Tools/makedist_cygwin

2014-05-30 blanchet [Fri, 30 May 2014 16:00:54 +0200] rev 57133
made 'Kuehlwein-style' be really like Python code, we now think
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

2014-05-30 blanchet [Fri, 30 May 2014 15:15:41 +0200] rev 57132
make SML code closer to Python code when 'nb_kuehlwein_style' is true
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

2014-05-30 blanchet [Fri, 30 May 2014 15:15:02 +0200] rev 57131
merge

2014-05-30 blanchet [Fri, 30 May 2014 14:43:06 +0200] rev 57130
added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

2014-05-30 hoelzl [Fri, 30 May 2014 14:55:10 +0200] rev 57129
introduce more powerful reindexing rules for big operators
src/HOL/Fact.thy src/HOL/Groups_Big.thy src/HOL/Library/Formal_Power_Series.thy src/HOL/Library/Permutations.thy src/HOL/Lifting_Set.thy src/HOL/Multivariate_Analysis/Determinants.thy src/HOL/Multivariate_Analysis/Integration.thy src/HOL/Multivariate_Analysis/PolyRoots.thy src/HOL/Number_Theory/Binomial.thy src/HOL/Old_Number_Theory/Finite2.thy src/HOL/Old_Number_Theory/Pocklington.thy src/HOL/Series.thy src/HOL/Set_Interval.thy src/HOL/Transcendental.thy

2014-05-30 wenzelm [Fri, 30 May 2014 12:54:42 +0200] rev 57128
merged

2014-05-30 wenzelm [Fri, 30 May 2014 11:02:02 +0200] rev 57127
make double-sure that old popup is dismissed, before replacing it;
src/Tools/jEdit/src/completion_popup.scala