moved adm_chfindom from Fix.thy to Cfun.thy
authorhuffman
Fri, 04 Nov 2005 23:15:11 +0100
changeset 18089 35c091a9841a
parent 18088 e5b23b85e932
child 18090 9d5cfd71f510
moved adm_chfindom from Fix.thy to Cfun.thy
src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Fri Nov 04 22:27:40 2005 +0100
+++ b/src/HOLCF/Cfun.thy	Fri Nov 04 23:15:11 2005 +0100
@@ -338,6 +338,9 @@
 apply (fast intro!: thelubI chfin lub_finch2 chfin2finch ch2ch_Rep_CFunL)
 done
 
+lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))"
+by (rule adm_subst, simp, rule adm_chfin)
+
 subsection {* Continuous injection-retraction pairs *}
 
 text {* Continuous retractions are strict. *}