Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
make Nitpick test a bit weaker;
authorblanchet
Wed, 10 Feb 2010 11:47:33 +0100
changeset 35087 e385fa507468
parent 35086 92a8c9ea5aa7
child 35089 17b7940f43e4
child 35177 168041f24f80
make Nitpick test a bit weaker; this should solve failure observed last night on "mac-poly"
src/HOL/Nitpick_Examples/Refute_Nits.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 10 08:54:56 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 10 11:47:33 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
isabelle