src/HOL/Product_Type.thy
changeset 44066 d74182c93f04
parent 43866 8a50dc70cbff
child 44921 58eef4843641
     1.1 --- a/src/HOL/Product_Type.thy	Mon Aug 08 10:26:26 2011 -0700
     1.2 +++ b/src/HOL/Product_Type.thy	Mon Aug 08 10:32:55 2011 -0700
     1.3 @@ -436,11 +436,11 @@
     1.4  
     1.5  lemmas surjective_pairing = pair_collapse [symmetric]
     1.6  
     1.7 -lemma Pair_fst_snd_eq: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
     1.8 +lemma prod_eq_iff: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
     1.9    by (cases s, cases t) simp
    1.10  
    1.11  lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
    1.12 -  by (simp add: Pair_fst_snd_eq)
    1.13 +  by (simp add: prod_eq_iff)
    1.14  
    1.15  lemma split_conv [simp, code]: "split f (a, b) = f a b"
    1.16    by (fact prod.cases)
    1.17 @@ -1226,4 +1226,6 @@
    1.18  
    1.19  lemmas split = split_conv  -- {* for backwards compatibility *}
    1.20  
    1.21 +lemmas Pair_fst_snd_eq = prod_eq_iff
    1.22 +
    1.23  end