author | bulwahn |
Wed, 21 Dec 2011 09:41:16 +0100 | |
changeset 45942 | 4dfb1f6bd99b |
parent 45941 | 2fd0bbf8be13 |
child 45943 | 8c4a5e664fbc |
--- 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 *}