--- a/src/HOL/Library/Saturated.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Library/Saturated.thy Wed Nov 04 08:13:52 2015 +0100
@@ -215,7 +215,7 @@
end
interpretation Inf_sat!: semilattice_neutr_set min "top :: 'a::len sat"
-where
+rewrites
"semilattice_neutr_set.F min (top :: 'a sat) = Inf"
proof -
show "semilattice_neutr_set min (top :: 'a sat)"
@@ -225,7 +225,7 @@
qed
interpretation Sup_sat!: semilattice_neutr_set max "bot :: 'a::len sat"
-where
+rewrites
"semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
proof -
show "semilattice_neutr_set max (bot :: 'a sat)"