src/HOL/HOLCF/Deflation.thy
changeset 41430 1aa23e9f2c87
parent 41182 717404c7d59a
child 42151 4da4fc77664b
     1.1 --- a/src/HOL/HOLCF/Deflation.thy	Tue Jan 04 15:03:27 2011 -0800
     1.2 +++ b/src/HOL/HOLCF/Deflation.thy	Tue Jan 04 15:32:56 2011 -0800
     1.3 @@ -56,7 +56,7 @@
     1.4  end
     1.5  
     1.6  lemma deflation_strict: "deflation d \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
     1.7 -by (rule deflation.below [THEN UU_I])
     1.8 +by (rule deflation.below [THEN bottomI])
     1.9  
    1.10  lemma adm_deflation: "adm (\<lambda>d. deflation d)"
    1.11  by (simp add: deflation_def)
    1.12 @@ -64,7 +64,7 @@
    1.13  lemma deflation_ID: "deflation ID"
    1.14  by (simp add: deflation.intro)
    1.15  
    1.16 -lemma deflation_UU: "deflation \<bottom>"
    1.17 +lemma deflation_bottom: "deflation \<bottom>"
    1.18  by (simp add: deflation.intro)
    1.19  
    1.20  lemma deflation_below_iff:
    1.21 @@ -160,7 +160,7 @@
    1.22    "finite_deflation d \<Longrightarrow> deflation d"
    1.23  unfolding finite_deflation_def by simp
    1.24  
    1.25 -lemma finite_deflation_UU: "finite_deflation \<bottom>"
    1.26 +lemma finite_deflation_bottom: "finite_deflation \<bottom>"
    1.27  by default simp_all
    1.28  
    1.29