src/HOL/Lattices_Big.thy
changeset 56993 e5366291d6aa
parent 56140 ed92ce2ac88e
child 57800 84748234de9d
     1.1 --- a/src/HOL/Lattices_Big.thy	Mon May 19 11:27:02 2014 +0200
     1.2 +++ b/src/HOL/Lattices_Big.thy	Mon May 19 12:04:45 2014 +0200
     1.3 @@ -125,6 +125,9 @@
     1.4    finally show ?case .
     1.5  qed
     1.6  
     1.7 +lemma infinite: "\<not> finite A \<Longrightarrow> F A = the None"
     1.8 +  unfolding eq_fold' by (cases "finite (UNIV::'a set)") (auto intro: finite_subset fold_infinite)
     1.9 +
    1.10  end
    1.11  
    1.12  locale semilattice_order_set = binary?: semilattice_order + semilattice_set