src/HOL/HOLCF/Library/Defl_Bifinite.thy

 apply (rule bifinite_approx_chain.defl_approx)
 apply (unfold bifinite_approx_chain_def)
 apply (rule someI_ex [OF bifinite])
 done
 
-instantiation defl :: (bifinite) liftdomain
+instantiation defl :: (bifinite) "domain"
 begin
 
 definition
   "emb = udom_emb defl_approx"
 

 definition
   "defl (t::'a defl itself) =
     (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))"
 
 definition
-  "(liftemb :: 'a defl u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
-
-definition
-  "(liftprj :: udom \<rightarrow> 'a defl u) = u_map\<cdot>prj oo u_prj"
-
-definition
-  "liftdefl (t::'a defl itself) = u_defl\<cdot>DEFL('a defl)"
-
-instance
-using liftemb_defl_def liftprj_defl_def liftdefl_defl_def
-proof (rule liftdomain_class_intro)
+  "(liftemb :: 'a defl u \<rightarrow> udom u) = u_map\<cdot>emb"
+
+definition
+  "(liftprj :: udom u \<rightarrow> 'a defl u) = u_map\<cdot>prj"
+
+definition
+  "liftdefl (t::'a defl itself) = pdefl\<cdot>DEFL('a defl)"
+
+instance proof
   show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a defl)"
     unfolding emb_defl_def prj_defl_def
     by (rule ep_pair_udom [OF defl_approx])
   show "cast\<cdot>DEFL('a defl) = emb oo (prj :: udom \<rightarrow> 'a defl)"
     unfolding defl_defl_def

     apply (simp add: Abs_fin_defl_inverse approx_chain.finite_deflation_approx [OF defl_approx]
                      ep_pair.finite_deflation_e_d_p [OF ep])
     apply (simp add: lub_distribs approx_chain.chain_approx [OF defl_approx]
                      approx_chain.lub_approx [OF defl_approx])
     done
-qed
+qed (fact liftemb_defl_def liftprj_defl_def liftdefl_defl_def)+
 
 end
 
 end