diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Finite_Set.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -1035,7 +1035,7 @@
 
 lemma inf_INF_fold_inf:
   assumes "finite A"
-  shows "inf B (INFI A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold") 
+  shows "inf B (INFIMUM A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold") 
 proof (rule sym)
   interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
   interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
@@ -1046,7 +1046,7 @@
 
 lemma sup_SUP_fold_sup:
   assumes "finite A"
-  shows "sup B (SUPR A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold") 
+  shows "sup B (SUPREMUM A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold") 
 proof (rule sym)
   interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
   interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
@@ -1057,12 +1057,12 @@
 
 lemma INF_fold_inf:
   assumes "finite A"
-  shows "INFI A f = fold (inf \<circ> f) top A"
+  shows "INFIMUM A f = fold (inf \<circ> f) top A"
   using assms inf_INF_fold_inf [of A top] by simp
 
 lemma SUP_fold_sup:
   assumes "finite A"
-  shows "SUPR A f = fold (sup \<circ> f) bot A"
+  shows "SUPREMUM A f = fold (sup \<circ> f) bot A"
   using assms sup_SUP_fold_sup [of A bot] by simp
 
 end