src/HOL/Library/Groups_Big_Fun.thy
changeset 67764 0f8cb5568b63
parent 66804 3f9bb52082c4
child 69164 74f1b0f10b2b
     1.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Sat Mar 03 22:33:25 2018 +0100
     1.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Sun Mar 04 12:22:48 2018 +0100
     1.3 @@ -215,8 +215,8 @@
     1.4  begin
     1.5  
     1.6  sublocale Sum_any: comm_monoid_fun plus 0
     1.7 +  rewrites "comm_monoid_set.F plus 0 = sum"
     1.8    defines Sum_any = Sum_any.G
     1.9 -  rewrites "comm_monoid_set.F plus 0 = sum"
    1.10  proof -
    1.11    show "comm_monoid_fun plus 0" ..
    1.12    then interpret Sum_any: comm_monoid_fun plus 0 .
    1.13 @@ -282,8 +282,8 @@
    1.14  begin
    1.15  
    1.16  sublocale Prod_any: comm_monoid_fun times 1
    1.17 +  rewrites "comm_monoid_set.F times 1 = prod"
    1.18    defines Prod_any = Prod_any.G
    1.19 -  rewrites "comm_monoid_set.F times 1 = prod"
    1.20  proof -
    1.21    show "comm_monoid_fun times 1" ..
    1.22    then interpret Prod_any: comm_monoid_fun times 1 .