--- a/src/HOLCF/Adm.thy Tue Jul 01 06:51:59 2008 +0200
+++ b/src/HOLCF/Adm.thy Tue Jul 01 06:56:37 2008 +0200
@@ -123,8 +123,6 @@
text {* admissibility and continuity *}
-declare range_composition [simp del]
-
lemma adm_less: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
apply (rule admI)
apply (simp add: cont2contlubE)
--- a/src/HOLCF/Algebraic.thy Tue Jul 01 06:51:59 2008 +0200
+++ b/src/HOLCF/Algebraic.thy Tue Jul 01 06:56:37 2008 +0200
@@ -9,8 +9,6 @@
imports Completion Fix Eventual
begin
-declare range_composition [simp del]
-
subsection {* Constructing finite deflations by iteration *}
lemma finite_deflation_imp_deflation:
--- a/src/HOLCF/Ffun.thy Tue Jul 01 06:51:59 2008 +0200
+++ b/src/HOLCF/Ffun.thy Tue Jul 01 06:56:37 2008 +0200
@@ -201,8 +201,6 @@
text {* the lub of a chain of continuous functions is continuous *}
-declare range_composition [simp del]
-
lemma contlub_lub_fun:
"\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> contlub (\<Squnion>i. F i)"
apply (rule contlubI)