src/HOLCF/Ssum.thy

 qed
 
 lemma finite_deflation_ssum_map:
   assumes "finite_deflation d1" and "finite_deflation d2"
   shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)"
-proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+proof (rule finite_deflation_intro)
   interpret d1: finite_deflation d1 by fact
   interpret d2: finite_deflation d2 by fact
   have "deflation d1" and "deflation d2" by fact+
   thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map)
   have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>