# HG changeset patch
# User berghofe
# Date 939983503 -7200
# Node ID 30fb773113a1139c9b2277dcfd2e81ab04cd820a
# Parent  7941ce81cb309034636b10e50ae046215b87c9fb
Documented thm_deps.

diff -r 7941ce81cb30 -r 30fb773113a1 doc-src/Ref/thm.tex
--- 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