made lemma visible
authornipkow
Fri, 10 Jan 2025 17:13:27 +0100
changeset 81760 828ddde811ad
parent 81759 1b817e64af3c
child 81761 a1dc03194053
made lemma visible
src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Jan 10 15:48:20 2025 +0000
+++ b/src/HOL/Product_Type.thy	Fri Jan 10 17:13:27 2025 +0100
@@ -990,8 +990,8 @@
 lemma snd_swap [simp]: "snd (prod.swap x) = fst x"
   by (cases x) simp
 
-lemma split_pairs:
-  "(A,B) = X \<longleftrightarrow> fst X = A \<and> snd X = B" and "X = (A,B) \<longleftrightarrow> fst X = A \<and> snd X = B" 
+lemma split_pairs: "(A,B) = X \<longleftrightarrow> fst X = A \<and> snd X = B"
+  and split_pairs2: "X = (A,B) \<longleftrightarrow> fst X = A \<and> snd X = B" 
   by auto
 
 text \<open>Disjoint union of a family of sets -- Sigma.\<close>