changeset 41287 | 029a6fc1bfb8 |
parent 41286 | 3d7685a4a5ff |
child 41288 | a19edebad961 |
--- a/src/HOL/HOLCF/LowerPD.thy Sun Dec 19 05:15:31 2010 -0800 +++ b/src/HOL/HOLCF/LowerPD.thy Sun Dec 19 06:34:41 2010 -0800 @@ -482,7 +482,7 @@ using lower_map_ID finite_deflation_lower_map unfolding lower_approx_def by (rule approx_chain_lemma1) -definition lower_defl :: "defl \<rightarrow> defl" +definition lower_defl :: "udom defl \<rightarrow> udom defl" where "lower_defl = defl_fun1 lower_approx lower_map" lemma cast_lower_defl: