--- a/src/HOL/Library/Groups_Big_Fun.thy Mon Jul 11 09:57:20 2016 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Mon Jul 11 10:43:27 2016 +0200
@@ -215,10 +215,8 @@
begin
sublocale Sum_any: comm_monoid_fun plus 0
-defines
- Sum_any = Sum_any.G
-rewrites
- "comm_monoid_set.F plus 0 = setsum"
+ defines Sum_any = Sum_any.G
+ rewrites "comm_monoid_set.F plus 0 = setsum"
proof -
show "comm_monoid_fun plus 0" ..
then interpret Sum_any: comm_monoid_fun plus 0 .
@@ -284,10 +282,8 @@
begin
sublocale Prod_any: comm_monoid_fun times 1
-defines
- Prod_any = Prod_any.G
-rewrites
- "comm_monoid_set.F times 1 = setprod"
+ defines Prod_any = Prod_any.G
+ rewrites "comm_monoid_set.F times 1 = setprod"
proof -
show "comm_monoid_fun times 1" ..
then interpret Prod_any: comm_monoid_fun times 1 .