Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Product_Type.thy
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"
isabelle