# HG changeset patch # User blanchet # Date 1289035508 -3600 # Node ID 8adcdd2c5805faaa5421a08841196ae98cae78f0 # Parent 3642dc3b72e8fa20232d7b0c9c71973507330385 make Nitpick datatype tests faster to make timeout less likely diff -r 3642dc3b72e8 -r 8adcdd2c5805 src/HOL/Nitpick_Examples/Datatype_Nits.thy --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Sat Nov 06 10:25:08 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Sat Nov 06 10:25:08 2010 +0100 @@ -23,7 +23,7 @@ "rot NibbleF = Nibble0" lemma "rot n \ n" -nitpick [card = 1\16, expect = none] +nitpick [card = 1\8,16, verbose, expect = none] sorry lemma "rot Nibble2 \ Nibble3" @@ -69,7 +69,7 @@ oops lemma "fs (Pd ((a, b), (c, d))) = (a, b)" -nitpick [card = 1\9, expect = none] +nitpick [expect = none] sorry lemma "fs (Pd ((a, b), (c, d))) = (c, d)" @@ -82,7 +82,7 @@ "app (Fn f) x = f x" lemma "app (Fn g) y = g y" -nitpick [card = 1\10, expect = none] +nitpick [expect = none] sorry lemma "app (Fn g) y = g' y"