remove_thy;
authorwenzelm
Mon, 17 May 1999 19:15:35 +0200
changeset 6658 b44dd06378cc
parent 6657 9627197bd9e1
child 6659 7a056250899d
remove_thy;
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,