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