Documented thm_deps.

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