# HG changeset patch
# User wenzelm
# Date 1286739730 -3600
# Node ID eacb7825025d56849007715f367cdfa5e96d3b70
# Parent  a194f39cfcb441a24fb76f9d2173ed9a35295683
cover some more theory operations;

diff -r a194f39cfcb4 -r eacb7825025d doc-src/IsarImplementation/Thy/Prelim.thy
--- 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.