src/HOL/Product_Type.thy
changeset 37704 c6161bee8486
parent 37678 0040bafffdef
child 37751 89e16802b6cc
     1.1 --- a/src/HOL/Product_Type.thy	Sat Jul 03 00:49:12 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Sat Jul 03 00:50:35 2010 +0200
     1.3 @@ -158,6 +158,8 @@
     1.4      by (simp add: Pair_def Abs_prod_inject)
     1.5  qed
     1.6  
     1.7 +declare prod.simps(2) [nitpick_simp del]
     1.8 +
     1.9  declare weak_case_cong [cong del]
    1.10  
    1.11  
    1.12 @@ -391,7 +393,7 @@
    1.13  code_const fst and snd
    1.14    (Haskell "fst" and "snd")
    1.15  
    1.16 -lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))"
    1.17 +lemma prod_case_unfold [nitpick_def]: "prod_case = (%c p. c (fst p) (snd p))"
    1.18    by (simp add: expand_fun_eq split: prod.split)
    1.19  
    1.20  lemma fst_eqD: "fst (x, y) = a ==> x = a"