# HG changeset patch
# User wenzelm
# Date 965237856 -7200
# Node ID 7e69882104889ae5da3ff8b9a147d644f35f6172
# Parent  b5d6db4111bca5e58bdd6f94c9f02ee26d008720
rep_thm: 'der' field has additional bool for oracles;

diff -r b5d6db4111bc -r 7e6988210488 doc-src/Ref/thm.tex
--- 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}