1.1 --- a/src/HOL/Set.thy	Mon Jul 13 08:25:43 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Jul 14 15:54:19 2009 +0200
     1.3 @@ -2249,10 +2249,10 @@
     1.4    unfolding Inf_Sup by auto
     1.5  
     1.6  lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
     1.7 -  by (auto intro: antisym Inf_greatest Inf_lower)
     1.8 +  by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
     1.9  
    1.10  lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    1.11 -  by (auto intro: antisym Sup_least Sup_upper)
    1.12 +  by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
    1.13  
    1.14  lemma Inf_singleton [simp]:
    1.15    "\<Sqinter>{a} = a"