# HG changeset patch # User nipkow # Date 1247391369 -7200 # Node ID f88e4f4948327f2caddb64be33c5c8c62da52731 # Parent 2ce88db62a841c6d1059de1744fbc129758b216f typo diff -r 2ce88db62a84 -r f88e4f494832 src/HOL/Finite_Set.thy --- 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 \ 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 \ ALL a:A. a \ b \ fold sup c A \ sup b c" by(rule lower_semilattice.inf_le_fold_inf)(rule dual_semilattice)