author | wenzelm |
Wed, 10 Feb 2010 12:04:57 +0100 | |
changeset 35089 | 17b7940f43e4 |
parent 35087 | e385fa507468 (diff) |
parent 35088 | 6591285a6a59 (current diff) |
child 35094 | a0e89e47b083 |
child 35098 | 45dec8e27c4b |
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 10 12:03:13 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 10 12:04:57 2010 +0100 @@ -885,7 +885,7 @@ done lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)" -nitpick [card = 1\<midarrow>6, expect = none] +nitpick [card = 1\<midarrow>5, expect = none] apply simp done