--- a/src/HOL/List.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/List.thy Sun Mar 16 18:09:04 2014 +0100
@@ -2877,13 +2877,13 @@
lemma (in complete_lattice) INF_set_fold:
"INFI (set xs) f = fold (inf \<circ> f) xs top"
- unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
+ using Inf_set_fold [of "map f xs "] by (simp add: fold_map)
declare INF_set_fold [code]
lemma (in complete_lattice) SUP_set_fold:
"SUPR (set xs) f = fold (sup \<circ> f) xs bot"
- unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
+ using Sup_set_fold [of "map f xs "] by (simp add: fold_map)
declare SUP_set_fold [code]