Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/IsarImplementation/Thy/document/integration.tex
changeset 27597 beb9b5f07dbc
parent 27492 77ec4ad35ca2 
--- 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
isabelle