src/HOL/Lattices.thy
changeset 26233 3751b3dbb67c
parent 26014 00c2c3525bef
child 26794 354c3844dfde
     1.1 --- a/src/HOL/Lattices.thy	Fri Mar 07 13:53:01 2008 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Fri Mar 07 13:53:02 2008 +0100
     1.3 @@ -354,36 +354,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 -  apply (rule antisym)
     1.8 -  apply (rule le_infI)
     1.9 -  apply (rule Inf_lower)
    1.10 -  apply simp
    1.11 -  apply (rule Inf_greatest)
    1.12 -  apply (rule Inf_lower)
    1.13 -  apply simp
    1.14 -  apply (rule Inf_greatest)
    1.15 -  apply (erule insertE)
    1.16 -  apply (rule le_infI1)
    1.17 -  apply simp
    1.18 -  apply (rule le_infI2)
    1.19 -  apply (erule Inf_lower)
    1.20 -  done
    1.21 +  by (auto intro: antisym Inf_greatest Inf_lower)
    1.22  
    1.23  lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    1.24 -  apply (rule antisym)
    1.25 -  apply (rule Sup_least)
    1.26 -  apply (erule insertE)
    1.27 -  apply (rule le_supI1)
    1.28 -  apply simp
    1.29 -  apply (rule le_supI2)
    1.30 -  apply (erule Sup_upper)
    1.31 -  apply (rule le_supI)
    1.32 -  apply (rule Sup_upper)
    1.33 -  apply simp
    1.34 -  apply (rule Sup_least)
    1.35 -  apply (rule Sup_upper)
    1.36 -  apply simp
    1.37 -  done
    1.38 +  by (auto intro: antisym Sup_least Sup_upper)
    1.39  
    1.40  lemma Inf_singleton [simp]:
    1.41    "\<Sqinter>{a} = a"