# HG changeset patch
# User nipkow
# Date 1736525607 -3600
# Node ID 828ddde811ad806d549e6716afe6a500da26f4ac
# Parent  1b817e64af3cf3d4f423891e49b8dc2f2ed5bba9
made lemma visible

diff -r 1b817e64af3c -r 828ddde811ad 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>