summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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