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