src/HOL/HOLCF/Adm.thy
changeset 41430 1aa23e9f2c87
parent 41182 717404c7d59a
child 41959 b460124855b8
     1.1 --- a/src/HOL/HOLCF/Adm.thy	Tue Jan 04 15:03:27 2011 -0800
     1.2 +++ b/src/HOL/HOLCF/Adm.thy	Tue Jan 04 15:32:56 2011 -0800
     1.3 @@ -175,7 +175,7 @@
     1.4    "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
     1.5  by (simp add: po_eq_conv)
     1.6  
     1.7 -lemma compact_UU [simp, intro]: "compact \<bottom>"
     1.8 +lemma compact_bottom [simp, intro]: "compact \<bottom>"
     1.9  by (rule compactI, simp)
    1.10  
    1.11  text {* Any upward-closed predicate is admissible. *}