# HG changeset patch
# User blanchet
# Date 1303208517 -7200
# Node ID 252ed2fc384d53b6efc51173449176cb93e346e0
# Parent  4a929b0630c3f8ca31a900ffa5dded14a098b024
remove a few Nitpick calls in examples -- another step toward making them run faster

diff -r 4a929b0630c3 -r 252ed2fc384d src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Apr 19 11:56:11 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Apr 19 12:21:57 2011 +0200
@@ -49,12 +49,10 @@
 
 lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y"
 nitpick [card = 1, expect = genuine]
-nitpick [card = 5, expect = genuine]
 oops
 
 lemma "P (\<lambda>x. x)"
 nitpick [card = 1, expect = genuine]
-nitpick [card = 5, expect = genuine]
 oops
 
 lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}"
@@ -95,7 +93,6 @@
 
 lemma "g = Let (A \<or> B)"
 nitpick [card = 1, expect = none]
-nitpick [card = 2, expect = genuine]
 nitpick [card = 12, expect = genuine]
 oops
 
@@ -122,7 +119,6 @@
 oops
 
 lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
-nitpick [card = 3, expect = genuine]
 nitpick [card = 3, dont_box, expect = genuine]
 nitpick [card = 8, expect = genuine]
 oops
@@ -144,7 +140,6 @@
 by auto
 
 lemma "f = split"
-nitpick [card = 1, expect = none]
 nitpick [card = 2, expect = genuine]
 oops
 
@@ -165,13 +160,11 @@
 
 lemma "x = y"
 nitpick [card 'a = 1, expect = none]
-nitpick [card 'a = 2, expect = genuine]
 nitpick [card 'a = 100, expect = genuine]
 oops
 
 lemma "\<forall>x. x = y"
 nitpick [card 'a = 1, expect = none]
-nitpick [card 'a = 2, expect = genuine]
 nitpick [card 'a = 100, expect = genuine]
 oops
 
@@ -251,7 +244,6 @@
 
 lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
 nitpick [card 'a = 1, expect = genuine]
-nitpick [card 'a = 5, expect = genuine]
 oops
 
 lemma "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x)
@@ -303,7 +295,6 @@
 lemma "x \<equiv> all \<Longrightarrow> False"
 nitpick [card = 1, expect = genuine]
 nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
-nitpick [card = 2, expect = genuine]
 nitpick [card = 6, expect = genuine]
 oops
 
@@ -329,7 +320,6 @@
 
 lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False"
 nitpick [card = 1, expect = genuine]
-nitpick [card = 20, expect = genuine]
 oops
 
 lemma "P x \<equiv> P x"
@@ -406,7 +396,6 @@
 
 lemma "x = All \<Longrightarrow> False"
 nitpick [card = 1, dont_box, expect = genuine]
-nitpick [card = 5, dont_box, expect = genuine]
 oops
 
 lemma "\<forall>x. f x y = f x y"
@@ -427,7 +416,6 @@
 
 lemma "x = Ex \<Longrightarrow> False"
 nitpick [card = 1, dont_box, expect = genuine]
-nitpick [card = 5, dont_box, expect = genuine]
 oops
 
 lemma "\<exists>x. f x y = f x y"
@@ -725,7 +713,6 @@
 
 lemma "P x \<Longrightarrow> P (The P)"
 nitpick [card = 1\<midarrow>2, expect = none]
-nitpick [card = 3, expect = genuine]
 nitpick [card = 8, expect = genuine]
 oops
 
diff -r 4a929b0630c3 -r 252ed2fc384d src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue Apr 19 11:56:11 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue Apr 19 12:21:57 2011 +0200
@@ -491,7 +491,6 @@
 
 lemma "(x\<Colon>nat) < x + y"
 nitpick [card = 1, expect = genuine]
-nitpick [card = 2-5, expect = genuine]
 oops
 
 text {* \<times> *}