--- 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.