diff -r 0bd014c32479 -r 252739089bc8 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Oct 16 11:03:48 2025 +0200
+++ b/src/HOL/Set.thy	Fri Oct 17 15:42:50 2025 +0100
@@ -1182,7 +1182,7 @@
   by (fact bot_unique)
 
 lemma not_psubset_empty [iff]: "\<not> (A < {})"
-  by (fact not_less_bot) (* FIXME: already simp *)
+  by (fact not_less_bot) (*already simp *)
 
 lemma Collect_subset [simp]: "{x\<in>A. P x} \<subseteq> A" by auto
 
@@ -1204,6 +1204,9 @@
 lemma Collect_conj_eq: "{x. P x \<and> Q x} = {x. P x} \<inter> {x. Q x}"
   by blast
 
+lemma Collect_conj_eq2: "{x \<in> A. P x \<and> Q x} = {x \<in> A. P x} \<inter> {x \<in> A. Q x}"
+  by blast
+
 lemma Collect_mono_iff: "Collect P \<subseteq> Collect Q \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x)"
   by blast