src/HOL/Product_Type.thy
changeset 41792 ff3cb0c418b7
parent 41505 6d19301074cf
child 42059 83f3dc509068
equal deleted inserted replaced
41791:01d722707a36 41792:ff3cb0c418b7
   390   unfolding snd_def by simp
   390   unfolding snd_def by simp
   391 
   391 
   392 code_const fst and snd
   392 code_const fst and snd
   393   (Haskell "fst" and "snd")
   393   (Haskell "fst" and "snd")
   394 
   394 
   395 lemma prod_case_unfold [nitpick_def]: "prod_case = (%c p. c (fst p) (snd p))"
   395 lemma prod_case_unfold [nitpick_unfold]: "prod_case = (%c p. c (fst p) (snd p))"
   396   by (simp add: fun_eq_iff split: prod.split)
   396   by (simp add: fun_eq_iff split: prod.split)
   397 
   397 
   398 lemma fst_eqD: "fst (x, y) = a ==> x = a"
   398 lemma fst_eqD: "fst (x, y) = a ==> x = a"
   399   by simp
   399   by simp
   400 
   400