--- a/src/HOL/Groups_List.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Groups_List.thy Wed Nov 04 08:13:52 2015 +0100
@@ -66,7 +66,7 @@
"listsum = monoid_list.F plus 0"
sublocale listsum!: monoid_list plus 0
-where
+rewrites
"monoid_list.F plus 0 = listsum"
proof -
show "monoid_list plus 0" ..
@@ -80,7 +80,7 @@
begin
sublocale listsum!: comm_monoid_list plus 0
-where
+rewrites
"monoid_list.F plus 0 = listsum"
proof -
show "comm_monoid_list plus 0" ..
@@ -89,7 +89,7 @@
qed
sublocale setsum!: comm_monoid_list_set plus 0
-where
+rewrites
"monoid_list.F plus 0 = listsum"
and "comm_monoid_set.F plus 0 = setsum"
proof -
@@ -333,7 +333,7 @@
"listprod = monoid_list.F times 1"
sublocale listprod!: monoid_list times 1
-where
+rewrites
"monoid_list.F times 1 = listprod"
proof -
show "monoid_list times 1" ..
@@ -347,7 +347,7 @@
begin
sublocale listprod!: comm_monoid_list times 1
-where
+rewrites
"monoid_list.F times 1 = listprod"
proof -
show "comm_monoid_list times 1" ..
@@ -356,7 +356,7 @@
qed
sublocale setprod!: comm_monoid_list_set times 1
-where
+rewrites
"monoid_list.F times 1 = listprod"
and "comm_monoid_set.F times 1 = setprod"
proof -