--- a/doc-src/Ref/thm.tex Wed Jan 18 11:36:04 1995 +0100
+++ b/doc-src/Ref/thm.tex Thu Jan 19 16:05:21 1995 +0100
@@ -166,7 +166,7 @@
\end{ttdescription}
-\subsection{Miscellaneous forward rules}
+\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules}
\index{theorems!standardizing}
\begin{ttbox}
standard : thm -> thm
@@ -209,6 +209,7 @@
nprems_of : thm -> int
tpairs_of : thm -> (term*term)list
stamps_of_thy : thm -> string ref list
+theory_of_thm : thm -> theory
dest_state : thm*int -> (term*term)list*term list*term*term
rep_thm : thm -> \{prop:term, hyps:term list,
maxidx:int, sign:Sign.sg\}
@@ -230,6 +231,9 @@
\item[\ttindexbold{stamps_of_thm} $thm$]
returns the \rmindex{stamps} of the signature associated with~$thm$.
+\item[\ttindexbold{theory_of_thm} $thm$]
+returns the theory associated with $thm$.
+
\item[\ttindexbold{dest_state} $(thm,i)$]
decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem