--- 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.
--- 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