src/HOL/List.thy
changeset 56166 9a241bc276cd
parent 56085 3d11892ea537
child 56218 1c3f1f2431f9
     1.1 --- a/src/HOL/List.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/List.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -2877,13 +2877,13 @@
     1.4  
     1.5  lemma (in complete_lattice) INF_set_fold:
     1.6    "INFI (set xs) f = fold (inf \<circ> f) xs top"
     1.7 -  unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
     1.8 +  using Inf_set_fold [of "map f xs "] by (simp add: fold_map)
     1.9  
    1.10  declare INF_set_fold [code]
    1.11  
    1.12  lemma (in complete_lattice) SUP_set_fold:
    1.13    "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
    1.14 -  unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
    1.15 +  using Sup_set_fold [of "map f xs "] by (simp add: fold_map)
    1.16  
    1.17  declare SUP_set_fold [code]
    1.18