--- a/doc-src/IsarImplementation/Thy/document/integration.tex Tue Jul 15 09:30:39 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Tue Jul 15 10:49:39 2008 +0200
@@ -441,7 +441,7 @@
\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.end\_theory}\verb|ThyInfo.end_theory: theory -> unit| \\
\indexml{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
\verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
\indexml{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
@@ -473,8 +473,7 @@
normally not invoked directly.
\item \verb|ThyInfo.end_theory| concludes the loading of a theory
- proper. An attached theory {\ML} file may be still loaded later on.
- This is function is normally not invoked directly.
+ proper and stores the result in the theory database.
\item \verb|ThyInfo.register_theory|~\isa{text\ thy} registers an
existing theory value with the theory loader database. There is no
--- a/doc-src/IsarImplementation/Thy/integration.thy Tue Jul 15 09:30:39 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/integration.thy Tue Jul 15 10:49:39 2008 +0200
@@ -371,7 +371,7 @@
@{index_ML ThyInfo.touch_thy: "string -> unit"} \\
@{index_ML ThyInfo.remove_thy: "string -> unit"} \\[1ex]
@{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
- @{index_ML ThyInfo.end_theory: "theory -> theory"} \\
+ @{index_ML ThyInfo.end_theory: "theory -> unit"} \\
@{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
@{verbatim "datatype action = Update | Outdate | Remove"} \\
@{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\
@@ -403,8 +403,7 @@
normally not invoked directly.
\item @{ML ThyInfo.end_theory} concludes the loading of a theory
- proper. An attached theory {\ML} file may be still loaded later on.
- This is function is normally not invoked directly.
+ proper and stores the result in the theory database.
\item @{ML ThyInfo.register_theory}~@{text "text thy"} registers an
existing theory value with the theory loader database. There is no