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 \ B) x y \ B x y" by (simp add: inf_fun_def) -lemma inf_Int_eq: "(\x. x \ R) \ (\x. x \ S) = (\x. x \ R \ S)" +lemma inf_Int_eq [pred_set_conv]: "(\x. x \ R) \ (\x. x \ S) = (\x. x \ R \ S)" by (simp add: inf_fun_def) lemma inf_Int_eq2 [pred_set_conv]: "(\x y. (x, y) \ R) \ (\x y. (x, y) \ S) = (\x y. (x, y) \ R \ S)"