--- a/src/HOL/Finite_Set.thy Sun Jul 12 11:25:56 2009 +0200
+++ b/src/HOL/Finite_Set.thy Sun Jul 12 11:36:09 2009 +0200
@@ -835,7 +835,7 @@
by (rule lower_semilattice.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
-by(rule lower_semilattice.fold_inf_insert)(rule dual_semlattice)
+by(rule lower_semilattice.fold_inf_insert)(rule dual_semilattice)
lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c"
by(rule lower_semilattice.inf_le_fold_inf)(rule dual_semilattice)