src/HOL/HOLCF/Cfun.thy

   for x y :: "'a::flat"
   by (drule ax_flat) simp
 
 lemma flat_codom: "f\<cdot>x = c \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
   for c :: "'b::flat"
-  apply (case_tac "f\<cdot>x = \<bottom>")
+  apply (cases "f\<cdot>x = \<bottom>")
    apply (rule disjI1)
    apply (rule bottomI)
    apply (erule_tac t="\<bottom>" in subst)
    apply (rule minimal [THEN monofun_cfun_arg])
   apply clarify