--- a/doc-src/Ref/thm.tex Thu Oct 14 17:40:22 1999 +0200
+++ b/doc-src/Ref/thm.tex Fri Oct 15 12:31:43 1999 +0200
@@ -830,10 +830,24 @@
Use {\tt Deriv.drop} with argument~1 to skip over the initial {\tt Theorem}
constructor.
-
\index{proof objects|)}
\index{theorems|)}
+\medskip
+
+The dependencies of theorems can be viewed using the function \ttindexbold{thm_deps}:
+\begin{ttbox}
+thm_deps [\(thm@1\), \(\ldots\), \(thm@n\)];
+\end{ttbox}
+generates the dependency graph of the theorems $thm@1$, $\ldots$, $thm@n$ and
+displays it using Isabelle's graph browser. This function expects derivations
+to be enabled. The structure \texttt{ThmDeps} contains the two functions
+\begin{ttbox}
+enable : unit -> unit
+disable : unit -> unit
+\end{ttbox}
+which set \texttt{keep_derivs} appropriately.
+
%%% Local Variables:
%%% mode: latex