# HG changeset patch
# User huffman
# Date 1117060224 -7200
# Node ID 757e1c4a80814d04e6d86fc84710d63f5b73a849
# Parent  e1364521a25054a8630e02fc343ceb93657f2163
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun

diff -r e1364521a250 -r 757e1c4a8081 src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Wed May 25 16:14:40 2005 +0200
+++ b/src/HOLCF/Adm.thy	Thu May 26 00:30:24 2005 +0200
@@ -6,7 +6,7 @@
 header {* Admissibility *}
 
 theory Adm
-imports Cfun
+imports Cont
 begin
 
 defaultsort cpo
@@ -58,18 +58,6 @@
 
 lemmas adm_chfin = chfin [THEN adm_max_in_chain, standard]
 
-text {* some lemmata for functions with flat/chfin domain/range types *}
-
-lemma adm_chfindom: "adm (%(u::'a::cpo->'b::chfin). P(u$s))"
-apply (unfold adm_def)
-apply (intro strip)
-apply (drule chfin_Rep_CFunR)
-apply (erule_tac x = "s" in allE)
-apply clarsimp
-done
-
-(* adm_flat not needed any more, since it is a special case of adm_chfindom *)
-
 text {* improved admissibility introduction *}
 
 lemma admI2:
@@ -268,7 +256,6 @@
 val admD = thm "admD";
 val adm_max_in_chain = thm "adm_max_in_chain";
 val adm_chfin = thm "adm_chfin";
-val adm_chfindom = thm "adm_chfindom";
 val admI2 = thm "admI2";
 val adm_less = thm "adm_less";
 val adm_conj = thm "adm_conj";
diff -r e1364521a250 -r 757e1c4a8081 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Wed May 25 16:14:40 2005 +0200
+++ b/src/HOLCF/Fix.thy	Thu May 26 00:30:24 2005 +0200
@@ -247,6 +247,18 @@
 apply assumption
 done
 
+text {* some lemmata for functions with flat/chfin domain/range types *}
+
+lemma adm_chfindom: "adm (%(u::'a::cpo->'b::chfin). P(u$s))"
+apply (unfold adm_def)
+apply (intro strip)
+apply (drule chfin_Rep_CFunR)
+apply (erule_tac x = "s" in allE)
+apply clarsimp
+done
+
+(* adm_flat not needed any more, since it is a special case of adm_chfindom *)
+
 text {* fixed point induction *}
 
 lemma fix_ind: