# HG changeset patch
# User haftmann
# Date 1310300059 -7200
# Node ID 4529a3c5660967bfbb1ee8031bc0a3b7be06c68e
# Parent  d2f7af6e993c1fccdf4b3bdea9c57274799d3e4b
more succinct proofs

diff -r d2f7af6e993c -r 4529a3c56609 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sat Jul 09 21:18:20 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 14:14:19 2011 +0200
@@ -359,16 +359,16 @@
   by (iprover intro: InterI subsetI dest: subsetD)
 
 lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
-  by blast
+  by (fact Inf_binary [symmetric])
 
 lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
   by (fact Inf_empty)
 
 lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
-  by blast
+  by (fact Inf_UNIV)
 
 lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
-  by blast
+  by (fact Inf_insert)
 
 lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
   by blast