--- a/NEWS Wed Feb 22 17:25:35 2012 +0100
+++ b/NEWS Wed Feb 22 18:08:27 2012 +0100
@@ -296,6 +296,9 @@
* Improved code generation of multisets.
+* New diagnostic command find_unused_assms to find potentially superfluous
+ assumptions in theorems using Quickcheck.
+
* Quickcheck:
- Quickcheck returns variable assignments as counterexamples, which
allows to reveal the underspecification of functions under test.
@@ -318,6 +321,8 @@
- Support for multisets.
+ - Added "use_subtype" options.
+
* Nitpick:
- Fixed infinite loop caused by the 'peephole_optim' option and
affecting 'rat' and 'real'.
--- a/src/HOL/IsaMakefile Wed Feb 22 17:25:35 2012 +0100
+++ b/src/HOL/IsaMakefile Wed Feb 22 18:08:27 2012 +0100
@@ -1513,7 +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/Find_Unused_Assms_Examples.thy \
Quickcheck_Examples/Quickcheck_Examples.thy \
Quickcheck_Examples/Quickcheck_Lattice_Examples.thy \
Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/Quickcheck_Examples/ROOT.ML Wed Feb 22 17:25:35 2012 +0100
+++ b/src/HOL/Quickcheck_Examples/ROOT.ML Wed Feb 22 18:08:27 2012 +0100
@@ -1,5 +1,5 @@
use_thys [
- "Find_Unused_Assms",
+ "Find_Unused_Assms_Examples",
"Quickcheck_Examples",
"Quickcheck_Lattice_Examples"
];