merged constants "split" and "prod_case" -- nitpick behaves differently
authorhaftmann
Mon, 28 Jun 2010 15:03:07 +0200
changeset 37590 180e80b4eac1
parent 37589 9c33d02656bc
child 37591 d3daea901123
merged constants "split" and "prod_case" -- nitpick behaves differently
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