--- a/doc-src/Ref/thm.tex Wed Aug 02 17:54:55 2000 +0200
+++ b/doc-src/Ref/thm.tex Wed Aug 02 19:37:36 2000 +0200
@@ -248,9 +248,9 @@
sign_of_thm : thm -> Sign.sg
theory_of_thm : thm -> theory
dest_state : thm * int -> (term*term) list * term list * term * term
-rep_thm : thm -> \{sign_ref: Sign.sg_ref, der: deriv, maxidx: int,
+rep_thm : thm -> \{sign_ref: Sign.sg_ref, der: bool * deriv, maxidx: int,
shyps: sort list, hyps: term list, prop: term\}
-crep_thm : thm -> \{sign_ref: Sign.sg_ref, der: deriv, maxidx: int,
+crep_thm : thm -> \{sign_ref: Sign.sg_ref, der: bool * deriv, maxidx: int,
shyps: sort list, hyps: cterm list, prop:{\ts}cterm\}
\end{ttbox}
\begin{ttdescription}