diff -r 3ea8ace6bc8a -r 1dd39517e1ce src/HOL/IMP/Abs_Int3.thy --- a/src/HOL/IMP/Abs_Int3.thy Fri Feb 07 10:44:04 2014 +0100 +++ b/src/HOL/IMP/Abs_Int3.thy Fri Feb 07 14:18:31 2014 +0100 @@ -596,7 +596,7 @@ lemma assumes "!!x y::'a::wn. x \ y \ f x \ f y" and "x \ f x" and "\ f x \ x" shows "x \ f x \ f(x \ f x)" -nitpick[card = 3, expect = genuine, show_consts] +nitpick[card = 3, expect = genuine, show_consts, timeout = 120] (* 1 < 2 < 3, f x = 2, @@ -613,7 +613,7 @@ lemma assumes "!!x y::'a::wn. x \ y \ f x \ f y" and "x \ f x" and "\ f x \ x" and "f(f x) \ f x" shows "f(x \ f x) \ x \ f x" -nitpick[card = 4, expect = genuine, show_consts] +nitpick[card = 4, expect = genuine, show_consts, timeout = 120] (* 0 < 1 < 2 < 3