extending quickcheck example
authorbulwahn
Wed, 21 Dec 2011 09:41:16 +0100
changeset 45942 4dfb1f6bd99b
parent 45941 2fd0bbf8be13
child 45943 8c4a5e664fbc
extending quickcheck example
src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Wed Dec 21 09:39:14 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Wed Dec 21 09:41:16 2011 +0100
@@ -347,11 +347,13 @@
 lemma
   "Dlist.length (Dlist.remove x xs) = Dlist.length xs - 1"
 quickcheck[exhaustive]
+quickcheck[random]
 oops
 
 lemma
   "Dlist.length (Dlist.insert x xs) = Dlist.length xs + 1"
 quickcheck[exhaustive]
+quickcheck[random]
 oops
 
 subsection {* Examples with Records *}