src/HOL/Complete_Lattice.thy
changeset 43739 4529a3c56609
parent 42284 326f57825e1a
child 43740 3316e6831801
     1.1 --- a/src/HOL/Complete_Lattice.thy	Sat Jul 09 21:18:20 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 14:14:19 2011 +0200
     1.3 @@ -359,16 +359,16 @@
     1.4    by (iprover intro: InterI subsetI dest: subsetD)
     1.5  
     1.6  lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
     1.7 -  by blast
     1.8 +  by (fact Inf_binary [symmetric])
     1.9  
    1.10  lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
    1.11    by (fact Inf_empty)
    1.12  
    1.13  lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
    1.14 -  by blast
    1.15 +  by (fact Inf_UNIV)
    1.16  
    1.17  lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
    1.18 -  by blast
    1.19 +  by (fact Inf_insert)
    1.20  
    1.21  lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
    1.22    by blast