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