--- a/doc-src/IsarImplementation/Thy/Integration.thy Tue Jul 20 23:09:49 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Integration.thy Tue Jul 20 23:16:21 2010 +0200
@@ -360,9 +360,9 @@
text %mlref {*
\begin{mldecls}
- @{index_ML theory: "string -> theory"} \\
@{index_ML use_thy: "string -> unit"} \\
@{index_ML use_thys: "string list -> unit"} \\
+ @{index_ML Thy_Info.get_theory: "string -> theory"} \\
@{index_ML Thy_Info.touch_thy: "string -> unit"} \\
@{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]
@{index_ML Thy_Info.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
@@ -374,10 +374,6 @@
\begin{description}
- \item @{ML theory}~@{text A} retrieves the theory value presently
- associated with name @{text A}. Note that the result might be
- outdated.
-
\item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully
up-to-date wrt.\ the external file store, reloading outdated
ancestors as required. In batch mode, the simultaneous @{ML
@@ -390,6 +386,10 @@
intrinsic parallelism can be exploited by the system, to speedup
loading.
+ \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value
+ presently associated with name @{text A}. Note that the result
+ might be outdated.
+
\item @{ML Thy_Info.touch_thy}~@{text A} performs and @{text outdate} action
on theory @{text A} and all descendants.