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}