src/HOL/Set.thy
changeset 32064 53ca12ff305d
parent 31991 37390299214a
child 32075 e8e0fb5da77a
child 32077 3698947146b2
--- a/src/HOL/Set.thy	Mon Jul 13 08:25:43 2009 +0200
+++ b/src/HOL/Set.thy	Tue Jul 14 15:54:19 2009 +0200
@@ -2249,10 +2249,10 @@
   unfolding Inf_Sup by auto
 
 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
-  by (auto intro: antisym Inf_greatest Inf_lower)
+  by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
 
 lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
-  by (auto intro: antisym Sup_least Sup_upper)
+  by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
 
 lemma Inf_singleton [simp]:
   "\<Sqinter>{a} = a"