--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 12 08:35:56 2014 +0100
@@ -519,18 +519,6 @@
nitpick [expect = genuine]
oops
-lemma "prod_rec f p = f (fst p) (snd p)"
-nitpick [expect = none]
-by (case_tac p) auto
-
-lemma "prod_rec f (a, b) = f a b"
-nitpick [expect = none]
-by auto
-
-lemma "P (prod_rec f x)"
-nitpick [expect = genuine]
-oops
-
lemma "P (case x of Pair a b \<Rightarrow> f a b)"
nitpick [expect = genuine]
oops
@@ -575,15 +563,6 @@
nitpick [expect = genuine]
oops
-lemma "unit_rec u x = u"
-nitpick [expect = none]
-apply simp
-done
-
-lemma "P (unit_rec u x)"
-nitpick [expect = genuine]
-oops
-
lemma "P (case x of () \<Rightarrow> u)"
nitpick [expect = genuine]
oops
@@ -646,20 +625,6 @@
nitpick [expect = genuine]
oops
-lemma "sum_rec l r (Inl x) = l x"
-nitpick [expect = none]
-apply simp
-done
-
-lemma "sum_rec l r (Inr x) = r x"
-nitpick [expect = none]
-apply simp
-done
-
-lemma "P (sum_rec l r x)"
-nitpick [expect = genuine]
-oops
-
lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
nitpick [expect = genuine]
oops