--- 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.
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex Tue Jul 20 23:09:49 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Tue Jul 20 23:16:21 2010 +0200
@@ -433,9 +433,9 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{theory}\verb|theory: string -> theory| \\
\indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\
\indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\
+ \indexdef{}{ML}{Thy\_Info.get\_theory}\verb|Thy_Info.get_theory: string -> theory| \\
\indexdef{}{ML}{Thy\_Info.touch\_thy}\verb|Thy_Info.touch_thy: string -> unit| \\
\indexdef{}{ML}{Thy\_Info.remove\_thy}\verb|Thy_Info.remove_thy: string -> unit| \\[1ex]
\indexdef{}{ML}{Thy\_Info.begin\_theory}\verb|Thy_Info.begin_theory|\verb|: ... -> bool -> theory| \\
@@ -447,10 +447,6 @@
\begin{description}
- \item \verb|theory|~\isa{A} retrieves the theory value presently
- associated with name \isa{A}. Note that the result might be
- outdated.
-
\item \verb|use_thy|~\isa{A} ensures that theory \isa{A} is fully
up-to-date wrt.\ the external file store, reloading outdated
ancestors as required. In batch mode, the simultaneous \verb|use_thys| should be used exclusively.
@@ -462,6 +458,10 @@
intrinsic parallelism can be exploited by the system, to speedup
loading.
+ \item \verb|Thy_Info.get_theory|~\isa{A} retrieves the theory value
+ presently associated with name \isa{A}. Note that the result
+ might be outdated.
+
\item \verb|Thy_Info.touch_thy|~\isa{A} performs and \isa{outdate} action
on theory \isa{A} and all descendants.