typo
authornipkow
Sun Jul 12 11:36:09 2009 +0200 (2009-07-12)
changeset 31994f88e4f494832
parent 31993 2ce88db62a84
child 31995 8f37cf60b885
typo
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Sun Jul 12 11:25:56 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Sun Jul 12 11:36:09 2009 +0200
     1.3 @@ -835,7 +835,7 @@
     1.4  by (rule lower_semilattice.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
     1.5  
     1.6  lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
     1.7 -by(rule lower_semilattice.fold_inf_insert)(rule dual_semlattice)
     1.8 +by(rule lower_semilattice.fold_inf_insert)(rule dual_semilattice)
     1.9  
    1.10  lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c"
    1.11  by(rule lower_semilattice.inf_le_fold_inf)(rule dual_semilattice)