diff -r 910d3ea1efa8 -r 0300d5170622 src/HOLCF/Algebraic.thy
--- a/src/HOLCF/Algebraic.thy	Thu Oct 07 13:22:13 2010 -0700
+++ b/src/HOLCF/Algebraic.thy	Thu Oct 07 13:33:06 2010 -0700
@@ -99,23 +99,10 @@
 using type_definition_sfp below_sfp_def
 by (rule below.typedef_ideal_cpo)
 
-lemma Rep_sfp_lub:
-  "chain Y \<Longrightarrow> Rep_sfp (\<Squnion>i. Y i) = (\<Union>i. Rep_sfp (Y i))"
-using type_definition_sfp below_sfp_def
-by (rule below.typedef_ideal_rep_contlub)
-
-lemma ideal_Rep_sfp: "below.ideal (Rep_sfp xs)"
-by (rule Rep_sfp [unfolded mem_Collect_eq])
-
 definition
   sfp_principal :: "fin_defl \<Rightarrow> sfp" where
   "sfp_principal t = Abs_sfp {u. u \<sqsubseteq> t}"
 
-lemma Rep_sfp_principal:
-  "Rep_sfp (sfp_principal t) = {u. u \<sqsubseteq> t}"
-unfolding sfp_principal_def
-by (simp add: Abs_sfp_inverse below.ideal_principal)
-
 lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
 proof
   have *: "\<And>d. finite (approx_chain.place udom_approx `
@@ -144,13 +131,9 @@
 qed
 
 interpretation sfp: ideal_completion below sfp_principal Rep_sfp
-apply default
-apply (rule ideal_Rep_sfp)
-apply (erule Rep_sfp_lub)
-apply (rule Rep_sfp_principal)
-apply (simp only: below_sfp_def)
-apply (rule fin_defl_countable)
-done
+using type_definition_sfp below_sfp_def
+using sfp_principal_def fin_defl_countable
+by (rule below.typedef_ideal_completion)
 
 text {* Algebraic deflations are pointed *}