# HG changeset patch
# User berghofe
# Date 1208337849 -7200
# Node ID 19e1d3c96f2f2b30406612e0001bb938e0fbc9cd
# Parent  18ff77116937a7291408295811b6cd580e93afaf
Added entry for unused_thms command.

diff -r 18ff77116937 -r 19e1d3c96f2f NEWS
--- a/NEWS	Wed Apr 16 11:01:30 2008 +0200
+++ b/NEWS	Wed Apr 16 11:24:09 2008 +0200
@@ -34,6 +34,32 @@
 
 *** Pure ***
 
+* Unused theorems can be found using the new command 'unused_thms'.
+There are three ways of invoking it:
+
+(1) unused_thms
+     Only finds unused theorems in the current theory.
+
+(2) unused_thms thy_1 ... thy_n -
+     Finds unused theorems in the current theory and all of its ancestors,
+     excluding the theories thy_1 ... thy_n and all of their ancestors.
+
+(3) unused_thms thy_1 ... thy_n - thy'_1 ... thy'_m
+     Finds unused theorems in the theories thy'_1 ... thy'_m and all of
+     their ancestors, excluding the theories thy_1 ... thy_n and all of
+     their ancestors.
+
+In order to increase the readability of the list produced by unused_thms,
+theorems that have been created by a particular instance of a theory
+command such as inductive or fun(ction) are considered to belong to the
+same "group", meaning that if at least one theorem in this group is used,
+the other theorems in the same group are no longer reported as unused.
+Moreover, if all theorems in the group are unused, only one theorem in
+the group is displayed.
+Note that proof objects have to be switched on in order for unused_thms
+to work properly (i.e. !proofs must be >= 1, which is usually the case
+when using ProofGeneral with the default settings).
+
 * Authentic naming of facts disallows ad-hoc overwriting of previous
 theorems within the same name space.  INCOMPATIBILITY, need to remove
 duplicate fact bindings, or even accidental fact duplications.  Note