src/HOL/Library/More_List.thy
changeset 44928 7ef6505bde7f
parent 44013 5cfc1c36ae97
child 45144 3f4742ce4629
child 45145 d5086da3c32d
     1.1 --- a/src/HOL/Library/More_List.thy	Wed Sep 14 10:55:07 2011 +0200
     1.2 +++ b/src/HOL/Library/More_List.thy	Wed Sep 14 10:08:52 2011 -0400
     1.3 @@ -262,11 +262,11 @@
     1.4  
     1.5  lemma (in complete_lattice) INFI_set_fold:
     1.6    "INFI (set xs) f = fold (inf \<circ> f) xs top"
     1.7 -  unfolding INFI_def set_map [symmetric] Inf_set_fold fold_map ..
     1.8 +  unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
     1.9  
    1.10  lemma (in complete_lattice) SUPR_set_fold:
    1.11    "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
    1.12 -  unfolding SUPR_def set_map [symmetric] Sup_set_fold fold_map ..
    1.13 +  unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
    1.14  
    1.15  text {* @{text nth_map} *}
    1.16