--- a/src/HOL/List.thy Tue Dec 31 22:18:31 2013 +0100
+++ b/src/HOL/List.thy Tue Dec 31 22:18:31 2013 +0100
@@ -2822,7 +2822,7 @@
"A \<inter> List.coset xs = fold Set.remove xs A"
by (simp add: Diff_eq [symmetric] minus_set_fold)
-lemma (in semilattice_set) set_eq_fold:
+lemma (in semilattice_set) set_eq_fold [code]:
"F (set (x # xs)) = fold f xs x"
proof -
interpret comp_fun_idem f
@@ -2830,11 +2830,6 @@
show ?thesis by (simp add: eq_fold fold_set_fold)
qed
-declare Inf_fin.set_eq_fold [code]
-declare Sup_fin.set_eq_fold [code]
-declare Min.set_eq_fold [code]
-declare Max.set_eq_fold [code]
-
lemma (in complete_lattice) Inf_set_fold:
"Inf (set xs) = fold inf xs top"
proof -