changeset 41792 | ff3cb0c418b7 |
parent 41505 | 6d19301074cf |
child 42059 | 83f3dc509068 |
--- a/src/HOL/Product_Type.thy Mon Feb 21 10:42:29 2011 +0100 +++ b/src/HOL/Product_Type.thy Mon Feb 21 10:44:19 2011 +0100 @@ -392,7 +392,7 @@ code_const fst and snd (Haskell "fst" and "snd") -lemma prod_case_unfold [nitpick_def]: "prod_case = (%c p. c (fst p) (snd p))" +lemma prod_case_unfold [nitpick_unfold]: "prod_case = (%c p. c (fst p) (snd p))" by (simp add: fun_eq_iff split: prod.split) lemma fst_eqD: "fst (x, y) = a ==> x = a"