--- a/src/HOL/Library/Dlist.thy Tue Dec 20 17:40:15 2011 +0100
+++ b/src/HOL/Library/Dlist.thy Tue Dec 20 17:40:17 2011 +0100
@@ -180,6 +180,9 @@
enriched_type map: map
by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
+subsection {* Quickcheck generators *}
+
+quickcheck_generator dlist constructors: empty, insert
hide_const (open) member fold foldr empty insert remove map filter null member length fold
--- a/src/HOL/ex/Quickcheck_Examples.thy Tue Dec 20 17:40:15 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy Tue Dec 20 17:40:17 2011 +0100
@@ -6,7 +6,7 @@
header {* Examples for the 'quickcheck' command *}
theory Quickcheck_Examples
-imports Complex_Main
+imports Complex_Main "~~/src/HOL/Library/Dlist"
begin
text {*
@@ -342,6 +342,17 @@
quickcheck[expect = counterexample]
oops
+subsection {* Examples with abstract types *}
+
+lemma
+ "Dlist.length (Dlist.remove x xs) = Dlist.length xs - 1"
+quickcheck[exhaustive]
+oops
+
+lemma
+ "Dlist.length (Dlist.insert x xs) = Dlist.length xs + 1"
+quickcheck[exhaustive]
+oops
subsection {* Examples with Records *}