# HG changeset patch
# User haftmann
# Date 1253716373 -7200
# Node ID 7f9e05b3d0fb33ff75f7ebd6b3fae2d1fc8e8579
# Parent  457135bdd59619146be3a9d9a0bc8a6abb1beaf7
removed potentially dangerous rules from pred_set_conv

diff -r 457135bdd596 -r 7f9e05b3d0fb src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Sep 23 16:32:53 2009 +0200
+++ b/src/HOL/Predicate.thy	Wed Sep 23 16:32:53 2009 +0200
@@ -81,7 +81,7 @@
 lemma sup2_iff: "sup A B x y \<longleftrightarrow> A x y | B x y"
   by (simp add: sup_fun_eq sup_bool_eq)
 
-lemma sup_Un_eq [pred_set_conv]: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
+lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
   by (simp add: sup1_iff expand_fun_eq)
 
 lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
@@ -125,7 +125,7 @@
 lemma inf2_iff: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
   by (simp add: inf_fun_eq inf_bool_eq)
 
-lemma inf_Int_eq [pred_set_conv]: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
+lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   by (simp add: inf1_iff expand_fun_eq)
 
 lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"