# HG changeset patch # User haftmann # Date 1534941178 0 # Node ID 567079abb17354d430ceab04dcc4554ffc5dc096 # Parent 54fdc8bc73a3b1adff0be1f20535a085981e3cc4 tuned whitespace diff -r 54fdc8bc73a3 -r 567079abb173 src/HOL/List.thy --- a/src/HOL/List.thy Wed Aug 22 12:32:57 2018 +0000 +++ b/src/HOL/List.thy Wed Aug 22 12:32:58 2018 +0000 @@ -2983,11 +2983,11 @@ lemma (in complete_lattice) INF_set_fold: "INFIMUM (set xs) f = fold (inf \ f) xs top" - using Inf_set_fold [of "map f xs "] by (simp add: fold_map) + using Inf_set_fold [of "map f xs"] by (simp add: fold_map) lemma (in complete_lattice) SUP_set_fold: "SUPREMUM (set xs) f = fold (sup \ f) xs bot" - using Sup_set_fold [of "map f xs "] by (simp add: fold_map) + using Sup_set_fold [of "map f xs"] by (simp add: fold_map) subsubsection \Fold variants: @{const foldr} and @{const foldl}\