# HG changeset patch
# User lcp
# Date 790913060 -3600
# Node ID 5c18634db55d97eaa350255c94bb5379354765cf
# Parent  a0b71a4bbe5efbeef2f98180b62afde098dc4b24
Under RS added cross reference to bind_thm

diff -r a0b71a4bbe5e -r 5c18634db55d doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Tue Jan 24 03:03:19 1995 +0100
+++ b/doc-src/Ref/thm.tex	Tue Jan 24 03:04:20 1995 +0100
@@ -80,7 +80,9 @@
 MRL : thm list list * thm list -> thm list     \hfill{\bf infix}
 \end{ttbox}
 Joining rules together is a simple way of deriving new rules.  These
-functions are especially useful with destruction rules.
+functions are especially useful with destruction rules.  To store
+the result in the theorem database, use \ttindex{bind_thm}
+(\S\ref{ExtractingAndStoringTheProvedTheorem}). 
 \begin{ttdescription}
 \item[\tt$thm@1$ RSN $(i,thm@2)$] \indexbold{*RSN} 
   resolves the conclusion of $thm@1$ with the $i$th premise of~$thm@2$.