# HG changeset patch
# User blanchet
# Date 1275079864 -7200
# Node ID 23ab9a5c41cf8443f866a7290a3112b6effb39ff
# Parent  d47fe9260c245c750e8f9a4eb1497ca5706b6dea
remove two examples, now that the definition of "fst" and "snd" has changed

diff -r d47fe9260c24 -r 23ab9a5c41cf src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri May 28 22:34:21 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri May 28 22:51:04 2010 +0200
@@ -638,14 +638,6 @@
 nitpick [expect = none]
 by (simp add: snd_def)
 
-lemma "fst p = (THE a. \<exists>b. p = Pair a b)"
-nitpick [expect = none]
-by (simp add: fst_def)
-
-lemma "snd p = (THE b. \<exists>a. p = Pair a b)"
-nitpick [expect = none]
-by (simp add: snd_def)
-
 lemma "I = (\<lambda>x. x) \<Longrightarrow> fst = (\<lambda>x. fst (I x))"
 nitpick [expect = none]
 by auto