--- a/doc-src/IsarImplementation/Thy/document/integration.tex Tue Jul 08 16:19:24 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Tue Jul 08 17:48:17 2008 +0200
@@ -438,8 +438,8 @@
\indexml{theory}\verb|theory: string -> theory| \\
\indexml{use\_thy}\verb|use_thy: string -> unit| \\
\indexml{use\_thys}\verb|use_thys: string list -> unit| \\
- \indexml{touch\_thy}\verb|touch_thy: string -> unit| \\
- \indexml{remove\_thy}\verb|remove_thy: string -> unit| \\[1ex]
+ \indexml{ThyInfo.touch\_thy}\verb|ThyInfo.touch_thy: string -> unit| \\
+ \indexml{ThyInfo.remove\_thy}\verb|ThyInfo.remove_thy: string -> unit| \\[1ex]
\indexml{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
\indexml{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> theory| \\
\indexml{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
@@ -462,10 +462,10 @@
import header of a theory, without performing the merge of the
result, though.
- \item \verb|touch_thy|~\isa{A} performs and \isa{outdate} action
+ \item \verb|ThyInfo.touch_thy|~\isa{A} performs and \isa{outdate} action
on theory \isa{A} and all descendants.
- \item \verb|remove_thy|~\isa{A} deletes theory \isa{A} and all
+ \item \verb|ThyInfo.remove_thy|~\isa{A} deletes theory \isa{A} and all
descendants from the theory database.
\item \verb|ThyInfo.begin_theory| is the basic operation behind a