Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added inf_Int_eq to pred_set_conv database as well
authorberghofe
Thu, 12 Jan 2012 00:13:37 +0100
changeset 46191 a88546428c2a
parent 46190 a42c5f23109f
child 46192 93eaaacc1955
Added inf_Int_eq to pred_set_conv database as well
src/HOL/Predicate.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle