src/HOL/Complete_Lattice.thy
changeset 32642 026e7c6a6d08
parent 32606 b5c3a8a75772
child 32678 de1f7d4da21a
     1.1 --- a/src/HOL/Complete_Lattice.thy	Mon Sep 21 16:11:36 2009 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Tue Sep 22 15:36:55 2009 +0200
     1.3 @@ -76,11 +76,11 @@
     1.4  
     1.5  lemma sup_bot [simp]:
     1.6    "x \<squnion> bot = x"
     1.7 -  using bot_least [of x] by (simp add: sup_commute)
     1.8 +  using bot_least [of x] by (simp add: sup_commute sup_absorb2)
     1.9  
    1.10  lemma inf_top [simp]:
    1.11    "x \<sqinter> top = x"
    1.12 -  using top_greatest [of x] by (simp add: inf_commute)
    1.13 +  using top_greatest [of x] by (simp add: inf_commute inf_absorb2)
    1.14  
    1.15  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.16    "SUPR A f = \<Squnion> (f ` A)"