--- a/src/HOL/Finite_Set.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Finite_Set.thy Wed Sep 14 10:08:52 2011 -0400
@@ -784,7 +784,7 @@
interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
from `finite A` show "?fold = ?inf"
by (induct A arbitrary: B)
- (simp_all add: INFI_def inf_left_commute)
+ (simp_all add: INF_def inf_left_commute)
qed
lemma sup_SUPR_fold_sup:
@@ -795,7 +795,7 @@
interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
from `finite A` show "?fold = ?sup"
by (induct A arbitrary: B)
- (simp_all add: SUPR_def sup_left_commute)
+ (simp_all add: SUP_def sup_left_commute)
qed
lemma INFI_fold_inf: