# HG changeset patch
# User huffman
# Date 1214887919 -7200
# Node ID 564117b58d73efc5302d9fba0e959050d8428431
# Parent  6cc897e2468a799100966a780cc88413374b8740
remove simp attribute from range_composition

diff -r 6cc897e2468a -r 564117b58d73 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Jul 01 06:21:28 2008 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jul 01 06:51:59 2008 +0200
@@ -255,7 +255,7 @@
 
 lemma finite_range_imageI:
     "finite (range g) ==> finite (range (%x. f (g x)))"
-  apply (drule finite_imageI, simp)
+  apply (drule finite_imageI, simp add: range_composition)
   done
 
 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
diff -r 6cc897e2468a -r 564117b58d73 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jul 01 06:21:28 2008 +0200
+++ b/src/HOL/Set.thy	Tue Jul 01 06:51:59 2008 +0200
@@ -1324,7 +1324,7 @@
 lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
   by auto
 
-lemma range_composition [simp]: "range (\<lambda>x. f (g x)) = f`range g"
+lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
 by (subst image_image, simp)
 
 
diff -r 6cc897e2468a -r 564117b58d73 src/HOL/SizeChange/Correctness.thy
--- a/src/HOL/SizeChange/Correctness.thy	Tue Jul 01 06:21:28 2008 +0200
+++ b/src/HOL/SizeChange/Correctness.thy	Tue Jul 01 06:51:59 2008 +0200
@@ -52,7 +52,7 @@
     neq: "\<And>x i. j x < i \<Longrightarrow> f i \<noteq> x" by blast
 
   from fin have "finite (range (j o f))" 
-    by (auto simp:comp_def)
+    by (auto simp:comp_def range_composition)
   with finite_nat_bounded
   obtain m where "range (j o f) \<subseteq> {..<m}" by blast
   hence "j (f m) < m" unfolding comp_def by auto