src/HOL/List.thy
changeset 44928 7ef6505bde7f
parent 44921 58eef4843641
child 45115 93c1ac6727a3
     1.1 --- a/src/HOL/List.thy	Wed Sep 14 10:55:07 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Sep 14 10:08:52 2011 -0400
     1.3 @@ -2549,12 +2549,12 @@
     1.4  
     1.5  lemma (in complete_lattice) INFI_set_fold:
     1.6    "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
     1.7 -  unfolding INFI_def set_map [symmetric] Inf_set_fold foldl_map
     1.8 +  unfolding INF_def set_map [symmetric] Inf_set_fold foldl_map
     1.9      by (simp add: inf_commute)
    1.10  
    1.11  lemma (in complete_lattice) SUPR_set_fold:
    1.12    "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
    1.13 -  unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
    1.14 +  unfolding SUP_def set_map [symmetric] Sup_set_fold foldl_map
    1.15      by (simp add: sup_commute)
    1.16  
    1.17  
    1.18 @@ -4987,8 +4987,8 @@
    1.19    "x \<in> set xs \<longleftrightarrow> member xs x"
    1.20    by (simp add: member_def)
    1.21  
    1.22 -declare INFI_def [code_unfold]
    1.23 -declare SUPR_def [code_unfold]
    1.24 +declare INF_def [code_unfold]
    1.25 +declare SUP_def [code_unfold]
    1.26  
    1.27  declare set_map [symmetric, code_unfold]
    1.28