src/HOLCF/Algebraic.thy

 by (rule typedef_po [OF type_definition_fin_defl sq_le_fin_defl_def])
 
 lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
 using Rep_fin_defl by simp
 
-interpretation Rep_fin_defl!: finite_deflation "Rep_fin_defl d"
+interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
 by (rule finite_deflation_Rep_fin_defl)
 
 lemma fin_defl_lessI:
   "(\<And>x. Rep_fin_defl a\<cdot>x = x \<Longrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a \<sqsubseteq> b"
 unfolding sq_le_fin_defl_def

 apply (rule profinite_compact_eq_approx)
 apply (erule subst)
 apply (rule Rep_fin_defl.compact)
 done
 
-interpretation fin_defl!: basis_take sq_le fd_take
+interpretation fin_defl: basis_take sq_le fd_take
 apply default
 apply (rule fd_take_less)
 apply (rule fd_take_idem)
 apply (erule fd_take_mono)
 apply (rule fd_take_chain, simp)

 lemma Rep_alg_defl_principal:
   "Rep_alg_defl (alg_defl_principal t) = {u. u \<sqsubseteq> t}"
 unfolding alg_defl_principal_def
 by (simp add: Abs_alg_defl_inverse sq_le.ideal_principal)
 
-interpretation alg_defl!:
+interpretation alg_defl:
   ideal_completion sq_le fd_take alg_defl_principal Rep_alg_defl
 apply default
 apply (rule ideal_Rep_alg_defl)
 apply (erule Rep_alg_defl_lub)
 apply (rule Rep_alg_defl_principal)

 apply (drule alg_defl.compact_imp_principal, clarify)
 apply (simp add: cast_alg_defl_principal)
 apply (rule finite_deflation_Rep_fin_defl)
 done
 
-interpretation cast!: deflation "cast\<cdot>d"
+interpretation cast: deflation "cast\<cdot>d"
 by (rule deflation_cast)
 
 lemma "cast\<cdot>(\<Squnion>i. alg_defl_principal (Abs_fin_defl (approx i)))\<cdot>x = x"
 apply (subst contlub_cfun_arg)
 apply (rule chainI)