--- a/doc-src/IsarImplementation/Thy/document/integration.tex Tue Jan 03 11:57:33 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Tue Jan 03 13:59:55 2006 +0100
@@ -394,7 +394,7 @@
been concluded, in order to support legacy proof {\ML} proof
scripts.
- The basic internal actions of the theory database are \isa{update}\indexbold{\isa{update} theory}, \isa{outdate}\indexbold{\isa{outdate} theory}, and \isa{remove}\indexbold{\isa{remove} theory}:
+ The basic internal actions of the theory database are \isa{update}, \isa{outdate}, and \isa{remove}:
\begin{itemize}