# HG changeset patch
# User nipkow
# Date 1389801564 -3600
# Node ID e2042c4ae1b78dd40455b7084ccac85e94edf4e2
# Parent  203b4f5482c32e9c43976e34860c88b281f2c64e
tuned text

diff -r 203b4f5482c3 -r e2042c4ae1b7 src/Doc/IsarRef/Misc.thy
--- a/src/Doc/IsarRef/Misc.thy	Wed Jan 15 08:01:36 2014 +0100
+++ b/src/Doc/IsarRef/Misc.thy	Wed Jan 15 16:59:24 2014 +0100
@@ -95,8 +95,9 @@
   tool (see also \cite{isabelle-sys}).
 
   \item @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"}
-  displays all unused theorems in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}
-  or their parents, but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents.
+  displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}
+  or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and
+  that are never used.
   If @{text n} is @{text 0}, the end of the range of theories
   defaults to the current theory. If no range is specified,
   only the unused theorems in the current theory are displayed.