# HG changeset patch
# User huffman
# Date 1131142511 -3600
# Node ID 35c091a9841a25038dd6695b4aa6ecc271daa5a4
# Parent  e5b23b85e9324b4bbb14535d61925116d35435d6
moved adm_chfindom from Fix.thy to Cfun.thy

diff -r e5b23b85e932 -r 35c091a9841a 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. *}