src/HOL/Groups_List.thy
changeset 61566 c3d6e570ccef
parent 61378 3e04c9ca001a
child 61605 1bf7b186542e
     1.1 --- a/src/HOL/Groups_List.thy	Wed Nov 04 08:13:49 2015 +0100
     1.2 +++ b/src/HOL/Groups_List.thy	Wed Nov 04 08:13:52 2015 +0100
     1.3 @@ -66,7 +66,7 @@
     1.4    "listsum  = monoid_list.F plus 0"
     1.5  
     1.6  sublocale listsum!: monoid_list plus 0
     1.7 -where
     1.8 +rewrites
     1.9   "monoid_list.F plus 0 = listsum"
    1.10  proof -
    1.11    show "monoid_list plus 0" ..
    1.12 @@ -80,7 +80,7 @@
    1.13  begin
    1.14  
    1.15  sublocale listsum!: comm_monoid_list plus 0
    1.16 -where
    1.17 +rewrites
    1.18    "monoid_list.F plus 0 = listsum"
    1.19  proof -
    1.20    show "comm_monoid_list plus 0" ..
    1.21 @@ -89,7 +89,7 @@
    1.22  qed
    1.23  
    1.24  sublocale setsum!: comm_monoid_list_set plus 0
    1.25 -where
    1.26 +rewrites
    1.27    "monoid_list.F plus 0 = listsum"
    1.28    and "comm_monoid_set.F plus 0 = setsum"
    1.29  proof -
    1.30 @@ -333,7 +333,7 @@
    1.31    "listprod  = monoid_list.F times 1"
    1.32  
    1.33  sublocale listprod!: monoid_list times 1
    1.34 -where
    1.35 +rewrites
    1.36    "monoid_list.F times 1 = listprod"
    1.37  proof -
    1.38    show "monoid_list times 1" ..
    1.39 @@ -347,7 +347,7 @@
    1.40  begin
    1.41  
    1.42  sublocale listprod!: comm_monoid_list times 1
    1.43 -where
    1.44 +rewrites
    1.45    "monoid_list.F times 1 = listprod"
    1.46  proof -
    1.47    show "comm_monoid_list times 1" ..
    1.48 @@ -356,7 +356,7 @@
    1.49  qed
    1.50  
    1.51  sublocale setprod!: comm_monoid_list_set times 1
    1.52 -where
    1.53 +rewrites
    1.54    "monoid_list.F times 1 = listprod"
    1.55    and "comm_monoid_set.F times 1 = setprod"
    1.56  proof -