# HG changeset patch
# User huffman
# Date 1214888197 -7200
# Node ID ff2a2b8fcd095af8477e17aaad9210d9f3897b90
# Parent  564117b58d73efc5302d9fba0e959050d8428431
range_composition no longer in simp set

diff -r 564117b58d73 -r ff2a2b8fcd09 src/HOLCF/Adm.thy
--- 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)
diff -r 564117b58d73 -r ff2a2b8fcd09 src/HOLCF/Algebraic.thy
--- 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:
diff -r 564117b58d73 -r ff2a2b8fcd09 src/HOLCF/Ffun.thy
--- 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)