changeset 1876 | b163e192a2bf |
parent 1846 | 763f08fb194f |
child 2040 | 6db93e6f1b11 |
--- a/doc-src/Ref/thm.tex Fri Jul 19 15:56:01 1996 +0200 +++ b/doc-src/Ref/thm.tex Mon Jul 22 16:15:00 1996 +0200 @@ -707,7 +707,7 @@ Deriv.size : deriv -> int Deriv.drop : 'a mtree * int -> 'a mtree Deriv.linear : deriv -> deriv list -Deriv.linear : deriv -> Deriv.orule mtree +Deriv.tree : deriv -> Deriv.orule mtree \end{ttbox} \begin{ttdescription}