# HG changeset patch
# User nipkow
# Date 1163363512 -3600
# Node ID 4d913b8bccf1c7087cc1df693f07e41adbc9b8e2
# Parent  be2669fe83634a9d0f7c5a15f02659cecdc691f1
image_constant_conv no longer [simp]

diff -r be2669fe8363 -r 4d913b8bccf1 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Sun Nov 12 21:14:52 2006 +0100
+++ b/src/HOL/FixedPoint.thy	Sun Nov 12 21:31:52 2006 +0100
@@ -112,7 +112,7 @@
 done
 
 lemma SUP_const[simp]: "(SUP i. M) = (M::'a::comp_lat)"
-by(simp add:SUP_def join_absorp1)
+by(simp add:SUP_def image_constant_conv join_absorp1)
 
 
 subsection {* Some instances of the type class of complete lattices *}
diff -r be2669fe8363 -r 4d913b8bccf1 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Nov 12 21:14:52 2006 +0100
+++ b/src/HOL/Set.thy	Sun Nov 12 21:31:52 2006 +0100
@@ -1231,7 +1231,7 @@
 lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
   by auto
 
-lemma image_constant_conv[simp]: "(%x. c) ` A = (if A = {} then {} else {c})"
+lemma image_constant_conv: "(%x. c) ` A = (if A = {} then {} else {c})"
 by auto
 
 lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"