# HG changeset patch
# User bulwahn
# Date 1329930507 -3600
# Node ID 1116909ef176775dfa20703ce53e4221f8ed8be0
# Parent  0a28a5a97d718170d55b89bf301319682021e92e
NEWS

diff -r 0a28a5a97d71 -r 1116909ef176 NEWS
--- 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'.
diff -r 0a28a5a97d71 -r 1116909ef176 src/HOL/IsaMakefile
--- 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
diff -r 0a28a5a97d71 -r 1116909ef176 src/HOL/Quickcheck_Examples/ROOT.ML
--- 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"
 ];