doc-src/IsarImplementation/Thy/integration.thy
changeset 18554 bff7a1466fe4
parent 18537 2681f9e34390
child 18558 48d5419fd191
--- a/doc-src/IsarImplementation/Thy/integration.thy	Tue Jan 03 11:57:33 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/integration.thy	Tue Jan 03 13:59:55 2006 +0100
@@ -321,9 +321,7 @@
   scripts.
 
   The basic internal actions of the theory database are @{text
-  "update"}\indexbold{@{text "update"} theory}, @{text
-  "outdate"}\indexbold{@{text "outdate"} theory}, and @{text
-  "remove"}\indexbold{@{text "remove"} theory}:
+  "update"}, @{text "outdate"}, and @{text "remove"}:
 
   \begin{itemize}