--- a/src/HOL/List.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/List.thy Wed Sep 14 10:08:52 2011 -0400
@@ -2549,12 +2549,12 @@
lemma (in complete_lattice) INFI_set_fold:
"INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
- unfolding INFI_def set_map [symmetric] Inf_set_fold foldl_map
+ unfolding INF_def set_map [symmetric] Inf_set_fold foldl_map
by (simp add: inf_commute)
lemma (in complete_lattice) SUPR_set_fold:
"SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
- unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
+ unfolding SUP_def set_map [symmetric] Sup_set_fold foldl_map
by (simp add: sup_commute)
@@ -4987,8 +4987,8 @@
"x \<in> set xs \<longleftrightarrow> member xs x"
by (simp add: member_def)
-declare INFI_def [code_unfold]
-declare SUPR_def [code_unfold]
+declare INF_def [code_unfold]
+declare SUP_def [code_unfold]
declare set_map [symmetric, code_unfold]