--- a/src/HOL/Library/Saturated.thy Mon Jul 11 09:57:20 2016 +0200
+++ b/src/HOL/Library/Saturated.thy Mon Jul 11 10:43:27 2016 +0200
@@ -215,8 +215,7 @@
end
interpretation Inf_sat: semilattice_neutr_set min "top :: 'a::len sat"
-rewrites
- "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
+ rewrites "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
proof -
show "semilattice_neutr_set min (top :: 'a sat)"
by standard (simp add: min_def)
@@ -225,8 +224,7 @@
qed
interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a::len sat"
-rewrites
- "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
+ rewrites "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
proof -
show "semilattice_neutr_set max (bot :: 'a sat)"
by standard (simp add: max_def bot.extremum_unique)