# HG changeset patch
# User haftmann
# Date 1253687151 -7200
# Node ID be4b248616c0db985e63ed8dd9c3cfb5018d3c21
# Parent  72e8608dce540de78180d34165ab82d13314fc82
inf/sup_absorb are no default simp rules any longer

diff -r 72e8608dce54 -r be4b248616c0 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Sep 22 15:39:46 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Sep 23 08:25:51 2009 +0200
@@ -1565,7 +1565,7 @@
   apply (rule finite_subset)
   prefer 2
   apply assumption
-  apply auto
+  apply (auto simp add: sup_absorb2)
 done
 
 lemma setsum_right_distrib: 
diff -r 72e8608dce54 -r be4b248616c0 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Tue Sep 22 15:39:46 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Wed Sep 23 08:25:51 2009 +0200
@@ -3649,7 +3649,7 @@
     from setsum_restrict_set[OF fS, of "\<lambda>v. u v *s v" S', symmetric] SS'
     have "setsum (\<lambda>v. ?u v *s v) S = setsum (\<lambda>v. u v *s v) S'"
       unfolding cond_value_iff cond_application_beta
-      by (simp add: cond_value_iff cong del: if_weak_cong)
+      by (simp add: cond_value_iff inf_absorb2 cong del: if_weak_cong)
     hence "setsum (\<lambda>v. ?u v *s v) S = y" by (metis u)
     hence "y \<in> ?rhs" by auto}
   moreover
diff -r 72e8608dce54 -r be4b248616c0 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Sep 22 15:39:46 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Wed Sep 23 08:25:51 2009 +0200
@@ -99,7 +99,7 @@
 
 lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast
 lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
-  apply (auto simp add: closedin_def Diff_Diff_Int)
+  apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2)
   apply (metis openin_subset subset_eq)
   done