# HG changeset patch
# User blanchet
# Date 1276591626 -7200
# Node ID df936eadb642b6e0164e8eea67657d259af00017
# Parent  a2a89563bfcb52c2d9ed642c652d5c20386e484b
make example run a bit faster (might help atbroy102)

diff -r a2a89563bfcb -r df936eadb642 src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jun 15 07:42:48 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jun 15 10:47:06 2010 +0200
@@ -1053,50 +1053,50 @@
 
 nitpick_params [full_descrs, max_potential = 1]
 
-lemma "(THE j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
-nitpick [card nat = 4, expect = potential]
-nitpick [card nat = 14, expect = potential] (* unfortunate *)
+lemma "(THE j. j > Suc 2 \<and> j \<le> 3) \<noteq> 0"
+nitpick [card nat = 2, expect = potential]
+nitpick [card nat = 6, expect = potential] (* unfortunate *)
 oops
 
-lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
-nitpick [card nat = 4, expect = potential]
-nitpick [card nat = 14, expect = none]
+lemma "(THE j. j > Suc 2 \<and> j \<le> 4) = x \<Longrightarrow> x \<noteq> 0"
+nitpick [card nat = 2, expect = potential]
+nitpick [card nat = 6, expect = none]
 sorry
 
-lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
-nitpick [card nat = 4, expect = potential]
-nitpick [card nat = 14, expect = none]
+lemma "(THE j. j > Suc 2 \<and> j \<le> 4) = x \<Longrightarrow> x = 4"
+nitpick [card nat = 2, expect = potential]
+nitpick [card nat = 6, expect = none]
 sorry
 
-lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
-nitpick [card nat = 14, expect = genuine]
+lemma "(THE j. j > Suc 2 \<and> j \<le> 5) = x \<Longrightarrow> x = 4"
+nitpick [card nat = 6, expect = genuine]
 oops
 
-lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
-nitpick [card nat = 14, expect = genuine]
+lemma "(THE j. j > Suc 2 \<and> j \<le> 5) = x \<Longrightarrow> x = 4 \<or> x = 5"
+nitpick [card nat = 6, expect = genuine]
 oops
 
-lemma "(SOME j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
-nitpick [card nat = 4, expect = potential]
-nitpick [card nat = 14, expect = genuine]
+lemma "(SOME j. j > Suc 2 \<and> j \<le> 3) \<noteq> 0"
+nitpick [card nat = 2, expect = potential]
+nitpick [card nat = 6, expect = genuine]
 oops
 
-lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
-nitpick [card nat = 4, expect = potential]
-nitpick [card nat = 14, expect = none]
+lemma "(SOME j. j > Suc 2 \<and> j \<le> 4) = x \<Longrightarrow> x \<noteq> 0"
+nitpick [card nat = 2, expect = potential]
+nitpick [card nat = 6, expect = none]
 oops
 
-lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
-nitpick [card nat = 4, expect = potential]
-nitpick [card nat = 14, expect = none]
+lemma "(SOME j. j > Suc 2 \<and> j \<le> 4) = x \<Longrightarrow> x = 4"
+nitpick [card nat = 2, expect = potential]
+nitpick [card nat = 6, expect = none]
 sorry
 
-lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
-nitpick [card nat = 14, expect = genuine]
+lemma "(SOME j. j > Suc 2 \<and> j \<le> 5) = x \<Longrightarrow> x = 4"
+nitpick [card nat = 6, expect = genuine]
 oops
 
-lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
-nitpick [card nat = 14, expect = none]
+lemma "(SOME j. j > Suc 2 \<and> j \<le> 5) = x \<Longrightarrow> x = 4 \<or> x = 5"
+nitpick [card nat = 6, expect = none]
 sorry
 
 nitpick_params [fast_descrs, max_potential = 0]