--- a/doc-src/IsarImplementation/Thy/Prelim.thy Sun Oct 10 20:12:10 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Sun Oct 10 20:42:10 2010 +0100
@@ -152,11 +152,14 @@
text %mlref {*
\begin{mldecls}
@{index_ML_type theory} \\
+ @{index_ML Theory.eq_thy: "theory * theory -> bool"} \\
@{index_ML Theory.subthy: "theory * theory -> bool"} \\
@{index_ML Theory.checkpoint: "theory -> theory"} \\
@{index_ML Theory.copy: "theory -> theory"} \\
@{index_ML Theory.merge: "theory * theory -> theory"} \\
@{index_ML Theory.begin_theory: "string -> theory list -> theory"} \\
+ @{index_ML Theory.parents_of: "theory -> theory list"} \\
+ @{index_ML Theory.ancestors_of: "theory -> theory list"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML_type theory_ref} \\
@@ -173,6 +176,9 @@
which the system does at least at the boundary of toplevel command
transactions \secref{sec:isar-toplevel}.
+ \item @{ML "Theory.eq_thy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} check strict
+ identity of two theories.
+
\item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} compares theories
according to the intrinsic graph structure of the construction.
This sub-theory relation is a nominal approximation of inclusion
@@ -196,6 +202,12 @@
a new theory based on the given parents. This ML function is
normally not invoked directly.
+ \item @{ML "Theory.parents_of"}~@{text "thy"} returns the direct
+ ancestors of @{text thy}.
+
+ \item @{ML "Theory.ancestors_of"}~@{text "thy"} returns all
+ ancestors of @{text thy} (not including @{text thy} itself).
+
\item @{ML_type theory_ref} represents a sliding reference to an
always valid theory; updates on the original are propagated
automatically.