# 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 \<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)