src/HOL/Library/Groups_Big_Fun.thy
changeset 61671 20d4cd2ceab2
parent 61670 301e0b4ecd45
child 61776 57bb7da5c867
     1.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Sat Nov 14 08:45:52 2015 +0100
     1.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Sat Nov 14 08:45:52 2015 +0100
     1.3 @@ -225,7 +225,7 @@
     1.4    "Sum_any = comm_monoid_fun.G plus 0"
     1.5  
     1.6  permanent_interpretation Sum_any: comm_monoid_fun plus 0
     1.7 -where
     1.8 +rewrites
     1.9    "comm_monoid_fun.G plus 0 = Sum_any" and
    1.10    "comm_monoid_set.F plus 0 = setsum"
    1.11  proof -
    1.12 @@ -298,7 +298,7 @@
    1.13    "Prod_any = comm_monoid_fun.G times 1"
    1.14  
    1.15  permanent_interpretation Prod_any: comm_monoid_fun times 1
    1.16 -where
    1.17 +rewrites
    1.18    "comm_monoid_fun.G times 1 = Prod_any" and
    1.19    "comm_monoid_set.F times 1 = setprod"
    1.20  proof -