author haftmann 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
--- 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