# HG changeset patch
# User berghofe
# Date 1326323617 -3600
# Node ID a88546428c2a099bc789a517a7a7f2e7ba5ba440
# Parent  a42c5f23109f0512a61f9a545da66a810f1c9733
Added inf_Int_eq to pred_set_conv database as well

diff -r a42c5f23109f -r a88546428c2a src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Jan 11 21:04:22 2012 +0100
+++ b/src/HOL/Predicate.thy	Thu Jan 12 00:13:37 2012 +0100
@@ -136,7 +136,7 @@
 lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
   by (simp add: inf_fun_def)
 
-lemma inf_Int_eq: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
+lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   by (simp add: inf_fun_def)
 
 lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"