# HG changeset patch
# User nipkow
# Date 1476985167 -7200
# Node ID 20d15328b248ef4c3157b02d8c38a9b08d2e4f0f
# Parent  95be866e49fc29a3ef995965c668f6e42d81f534# Parent  72060e61ca9df7652cbea19517484e280a4355f2
tuned

diff -r 95be866e49fc -r 20d15328b248 NEWS
--- a/NEWS	Thu Oct 20 18:42:01 2016 +0200
+++ b/NEWS	Thu Oct 20 19:39:27 2016 +0200
@@ -281,6 +281,9 @@
     mod_1 ~> mod_by_Suc_0
 INCOMPATIBILITY.
 
+* Renamed constants "setsum" ~> "sum" and "setprod" ~> "prod".
+  Corresponding renaming of theorems.
+
 * New type class "idom_abs_sgn" specifies algebraic properties
 of sign and absolute value functions.  Type class "sgn_if" has
 disappeared.  Slight INCOMPATIBILITY.
diff -r 95be866e49fc -r 20d15328b248 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Oct 20 18:42:01 2016 +0200
+++ b/src/HOL/ROOT	Thu Oct 20 19:39:27 2016 +0200
@@ -181,7 +181,7 @@
   theories [document = false]
     "Less_False"
     "~~/src/HOL/Library/Multiset"
-    "~~/src/HOL/Library/Float"
+    "~~/src/HOL/Number_Theory/Fib"
   theories
     Balance
     Tree_Map