Added a sentence in :doc rule-classes following feedback from Mihir M…

…ehta.

books/system/doc/acl2-doc.lisp

@@ -75408,9 +75408,9 @@ it."
 
 ;   (defstobj myarr (myarray-field :type (array (integer 0 *) (0))
 ;                                  :initially 0 :resizable t))
-;   
+;
 ;   (defstobj myparent (parent-arr :type myarr))
-;   
+;
 ;   (defun myparent-resize-array (size myparent)
 ;     (declare (xargs :stobjs myparent :guard (natp size)
 ;                     :guard-hints (("goal" :do-not-induct t))))
@@ -89030,7 +89030,8 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.</p>")
  arguments to the prover.  Such auxiliary proofs give the sort of output that
  one expects from the prover.  However, as noted above, corollaries that follow
  trivially are not submitted to the prover; thus, such corollaries cause no
- prover output.</p>
+ prover output.  Note that no rule is stored for the theorem until all
+ corollaries have been proved.</p>
 
  <p>Note that before @('term') is stored, all calls of macros in it are
  expanded away.  See @(see trans).</p>

doc.lisp

@@ -90165,7 +90165,9 @@ Subtopics
       as arguments to the prover. Such auxiliary proofs give the sort
       of output that one expects from the prover. However, as noted
       above, corollaries that follow trivially are not submitted to
-      the prover; thus, such corollaries cause no prover output.
+      the prover; thus, such corollaries cause no prover output. Note
+      that no rule is stored for the theorem until all corollaries
+      have been proved.
 
       Note that before term is stored, all calls of macros in it are
       expanded away. See [trans].