src/HOL/Predicate.thy
 changeset 32703 7f9e05b3d0fb parent 32601 47d0c967c64e child 32705 04ce6bb14d85
```     1.1 --- a/src/HOL/Predicate.thy	Wed Sep 23 16:32:53 2009 +0200
1.2 +++ b/src/HOL/Predicate.thy	Wed Sep 23 16:32:53 2009 +0200
1.3 @@ -81,7 +81,7 @@
1.4  lemma sup2_iff: "sup A B x y \<longleftrightarrow> A x y | B x y"
1.5    by (simp add: sup_fun_eq sup_bool_eq)
1.6
1.7 -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)"
1.8 +lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
1.9    by (simp add: sup1_iff expand_fun_eq)
1.10
1.11  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)"
1.12 @@ -125,7 +125,7 @@
1.13  lemma inf2_iff: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
1.14    by (simp add: inf_fun_eq inf_bool_eq)
1.15
1.16 -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)"
1.17 +lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
1.18    by (simp add: inf1_iff expand_fun_eq)
1.19
1.20  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)"
```