--- a/src/HOL/Library/FSet.thy Sat Mar 03 22:33:25 2018 +0100
+++ b/src/HOL/Library/FSet.thy Sun Mar 04 12:22:48 2018 +0100
@@ -751,8 +751,8 @@
context comm_monoid_add begin
sublocale fsum: comm_monoid_fset plus 0
+ rewrites "comm_monoid_set.F plus 0 = sum"
defines fsum = fsum.F
- rewrites "comm_monoid_set.F plus 0 = sum"
proof -
show "comm_monoid_fset (+) 0" by standard
@@ -797,8 +797,8 @@
context linorder begin
sublocale fMin: semilattice_order_fset min less_eq less
+ rewrites "semilattice_set.F min = Min"
defines fMin = fMin.F
- rewrites "semilattice_set.F min = Min"
proof -
show "semilattice_order_fset min (\<le>) (<)" by standard
@@ -806,8 +806,8 @@
qed
sublocale fMax: semilattice_order_fset max greater_eq greater
+ rewrites "semilattice_set.F max = Max"
defines fMax = fMax.F
- rewrites "semilattice_set.F max = Max"
proof -
show "semilattice_order_fset max (\<ge>) (>)"
by standard