--- a/src/HOL/Library/Groups_Big_Fun.thy Sat Mar 03 22:33:25 2018 +0100
+++ b/src/HOL/Library/Groups_Big_Fun.thy Sun Mar 04 12:22:48 2018 +0100
@@ -215,8 +215,8 @@
begin
sublocale Sum_any: comm_monoid_fun plus 0
+ rewrites "comm_monoid_set.F plus 0 = sum"
defines Sum_any = Sum_any.G
- rewrites "comm_monoid_set.F plus 0 = sum"
proof -
show "comm_monoid_fun plus 0" ..
then interpret Sum_any: comm_monoid_fun plus 0 .
@@ -282,8 +282,8 @@
begin
sublocale Prod_any: comm_monoid_fun times 1
+ rewrites "comm_monoid_set.F times 1 = prod"
defines Prod_any = Prod_any.G
- rewrites "comm_monoid_set.F times 1 = prod"
proof -
show "comm_monoid_fun times 1" ..
then interpret Prod_any: comm_monoid_fun times 1 .