# HG changeset patch
# User wenzelm
# Date 926961335 -7200
# Node ID b44dd06378ccf911b123a4ca414f400154cf0654
# Parent  9627197bd9e10468e208c629be83a9135f76c87b
remove_thy;

diff -r 9627197bd9e1 -r b44dd06378cc doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Mon May 17 18:00:59 1999 +0200
+++ b/doc-src/Ref/theories.tex	Mon May 17 19:15:35 1999 +0200
@@ -248,6 +248,7 @@
 use_thy_only    : string -> unit
 update_thy      : string -> unit
 touch_thy       : string -> unit
+remove_thy      : string -> unit
 delete_tmpfiles : bool ref \hfill{\bf initially true}
 \end{ttbox}
 
@@ -266,6 +267,11 @@
   internal graph as outdated.  While the theory remains usable, subsequent
   operations such as \texttt{use_thy} may cause a reload.
   
+\item[\ttindexbold{remove_thy} "$name$";] deletes theory node $name$,
+  including \emph{all} of its descendants.  Beware!  This is a quick way to
+  dispose a large number of theories at once.  Note that {\ML} bindings to
+  theorems etc.\ of removed theories may still persist.
+  
 \item[reset \ttindexbold{delete_tmpfiles};] processing theory files usually
   involves temporary {\ML} files to be created.  By default, these are deleted
   afterwards.  Resetting the \texttt{delete_tmpfiles} flag inhibits this,