# HG changeset patch
# User haftmann
# Date 1277730187 -7200
# Node ID 180e80b4eac1fb532b59b06ec54fa59f74968c7e
# Parent  9c33d02656bc3641b0fae40fc106839933d753c3
merged constants "split" and "prod_case" -- nitpick behaves differently

diff -r 9c33d02656bc -r 180e80b4eac1 src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Jun 28 15:03:06 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Jun 28 15:03:07 2010 +0200
@@ -17,11 +17,11 @@
 subsection {* Curry in a Hurry *}
 
 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
 by auto
 
 lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
 by auto
 
 lemma "split (curry f) = f"
@@ -61,12 +61,12 @@
 by auto
 
 lemma "split o curry = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
 apply (rule ext)+
 by auto
 
 lemma "curry o split = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
 apply (rule ext)+
 by auto