--- a/src/HOL/IsaMakefile Wed Feb 22 17:22:53 2012 +0100
+++ b/src/HOL/IsaMakefile Wed Feb 22 17:25:35 2012 +0100
@@ -1513,6 +1513,7 @@
HOL-Quickcheck_Examples: HOL $(LOG)/HOL-Quickcheck_Examples.gz
$(LOG)/HOL-Quickcheck_Examples.gz: $(OUT)/HOL \
+ Quickcheck_Examples/Find_Unused_Assms.thy \
Quickcheck_Examples/Quickcheck_Examples.thy \
Quickcheck_Examples/Quickcheck_Lattice_Examples.thy \
Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy Wed Feb 22 17:25:35 2012 +0100
@@ -0,0 +1,27 @@
+theory Find_Unused_Assms_Examples
+imports Main
+begin
+
+section {* Arithmetics *}
+
+declare [[quickcheck_finite_types = false]]
+
+find_unused_assms Divides
+find_unused_assms GCD
+find_unused_assms MacLaurin
+
+section {* Set Theory *}
+
+declare [[quickcheck_finite_types = true]]
+
+find_unused_assms Fun
+find_unused_assms Relation
+find_unused_assms Set
+find_unused_assms Wellfounded
+
+section {* Datatypes *}
+
+find_unused_assms List
+find_unused_assms Map
+
+end
\ No newline at end of file
--- a/src/HOL/Quickcheck_Examples/ROOT.ML Wed Feb 22 17:22:53 2012 +0100
+++ b/src/HOL/Quickcheck_Examples/ROOT.ML Wed Feb 22 17:25:35 2012 +0100
@@ -1,4 +1,5 @@
use_thys [
+ "Find_Unused_Assms",
"Quickcheck_Examples",
"Quickcheck_Lattice_Examples"
];