fight spurious nitpick timeouts
authornipkow
Fri, 07 Feb 2014 14:18:31 +0100
changeset 566991dd39517e1ce
parent 56698 3ea8ace6bc8a
child 56700 85d81bc281d0
child 56701 2d8222c76020
fight spurious nitpick timeouts
src/HOL/IMP/Abs_Int3.thy
     1.1 --- a/src/HOL/IMP/Abs_Int3.thy	Fri Feb 07 10:44:04 2014 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Fri Feb 07 14:18:31 2014 +0100
     1.3 @@ -596,7 +596,7 @@
     1.4  
     1.5  lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y"
     1.6  and "x \<le> f x" and "\<not> f x \<le> x" shows "x \<nabla> f x \<le> f(x \<nabla> f x)"
     1.7 -nitpick[card = 3, expect = genuine, show_consts]
     1.8 +nitpick[card = 3, expect = genuine, show_consts, timeout = 120]
     1.9  (*
    1.10  1 < 2 < 3,
    1.11  f x = 2,
    1.12 @@ -613,7 +613,7 @@
    1.13  lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y"
    1.14  and "x \<le> f x" and "\<not> f x \<le> x" and "f(f x) \<le> f x"
    1.15  shows "f(x \<nabla> f x) \<le> x \<nabla> f x"
    1.16 -nitpick[card = 4, expect = genuine, show_consts]
    1.17 +nitpick[card = 4, expect = genuine, show_consts, timeout = 120]
    1.18  (*
    1.19  
    1.20     0 < 1 < 2 < 3