src/HOL/Library/Quickcheck_Types.thy

--- a/src/HOL/Library/Quickcheck_Types.thy	Fri Jul 11 15:35:11 2014 +0200
+++ b/src/HOL/Library/Quickcheck_Types.thy	Fri Jul 11 15:52:03 2014 +0200
@@ -466,12 +466,4 @@
 
 hide_type non_distrib_lattice flat_complete_lattice bot top
 
-lemma "\<lbrakk> inf x z = inf y z; sup x z = sup y z \<rbrakk> \<Longrightarrow> x = y" 
-quickcheck[exhaustive, expect=counterexample]
-oops
-
-lemma "Inf {} = bot"
-quickcheck[exhaustive, expect=counterexample]
-oops
-
 end
\ No newline at end of file