--- a/src/HOL/List.thy Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/List.thy Mon Aug 20 10:44:53 2018 +0000
@@ -2985,14 +2985,10 @@
"INFIMUM (set xs) f = fold (inf \<circ> f) xs top"
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:
"SUPREMUM (set xs) f = fold (sup \<circ> f) xs bot"
using Sup_set_fold [of "map f xs "] by (simp add: fold_map)
-declare SUP_set_fold [code]
-
subsubsection \<open>Fold variants: @{const foldr} and @{const foldl}\<close>