# HG changeset patch
# User wenzelm
# Date 1389808978 -3600
# Node ID 869f50dfdad21a36c39481636f2db9b6a6d3f4fb
# Parent  e2042c4ae1b78dd40455b7084ccac85e94edf4e2# Parent  e6cfa56a8bcda51fe4fe66adcd3e5523eebe9e16
merged

diff -r e6cfa56a8bcd -r 869f50dfdad2 src/Doc/IsarRef/Misc.thy
--- a/src/Doc/IsarRef/Misc.thy	Wed Jan 15 16:57:29 2014 +0100
+++ b/src/Doc/IsarRef/Misc.thy	Wed Jan 15 19:02:58 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.