diff --git a/books/system/doc/acl2-doc.lisp b/books/system/doc/acl2-doc.lisp
index 15fe9c5c8eb..35baa810a74 100644
--- a/books/system/doc/acl2-doc.lisp
+++ b/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>
diff --git a/doc.lisp b/doc.lisp
index b20572ee765..5445f4cd4cc 100644
--- a/doc.lisp
+++ b/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].