diff --git a/big-unifier.mm b/big-unifier.mm
index 629cb9c8f7..9c936347e1 100644
--- a/big-unifier.mm
+++ b/big-unifier.mm
@@ -89,7 +89,7 @@ Dwight Megill (1950--2021).  For more information, visit
 
   $( A three-step proof that applies ~ ax-mp to the two axioms.  The proof was
      saved in compressed format with "SAVE PROOF theorem1 / COMPRESSED" in the
-     Metamath program. $)
+     Metamath program.  (Contributed by NM, 30-Aug-2008.) $)
   theorem1 $p |- e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) )
     , u ) ) ) , v ) , e ( x , v ) ) $=
     ( wi ax-min ax-maj ax-mp ) ABBCFECFFEFFZFZKDFADFFZAFZFJMFFZKNJFFNFZFAOFFZMP
@@ -98,7 +98,7 @@ Dwight Megill (1950--2021).  For more information, visit
   $( This is the same as ~ theorem1 , except that the proof is saved in
      uncompressed format with "SAVE PROOF theorem1u / NORMAL" in the Metamath
      program.  Note the size difference in the compressed versus uncompressed
-     proofs. $)
+     proofs.  (Contributed by NM, 30-Aug-2008.) $)
   theorem1u $p |- e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) )
     , u ) ) ) , v ) , e ( x , v ) ) $=
     wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi
diff --git a/demo0.mm b/demo0.mm
index e89d192b27..367ed1c67c 100644
--- a/demo0.mm
+++ b/demo0.mm
@@ -73,7 +73,7 @@ Dwight Megill (1950--2021).  For more information, visit
     mp $a |- Q $.
   $}
 
-  $( Prove a theorem. $)
+  $( Prove a theorem.  (Contributed by NM, 1-Jan-2004.) $)
   th1 $p |- t = t $=
   $( Here is its proof: $)
     tt tze tpl tt weq tt tt weq tt a2 tt tze tpl tt weq tt tze tpl tt weq tt tt
diff --git a/nf.mm b/nf.mm
index d2c34df2bf..7611415e07 100644
--- a/nf.mm
+++ b/nf.mm
@@ -19058,7 +19058,7 @@ might think (incorrectly) that it could be defined by ` E! x E! y ph ` .
        definitions.  This theorem shows that the erroneous definition can be
        repaired by conjoining ` A. x E* y ph ` as an additional condition.  The
        correct definition apparently has never been published.  ( ` E* ` means
-       "there exists at most one".) (Contributed by NM, 26-Oct-2003.) $)
+       "there exists at most one".)  (Contributed by NM, 26-Oct-2003.) $)
     2eu5 $p |- ( ( E! x E! y ph /\ A. x E* y ph ) <->
       ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) ) $=
       ( weu wmo wal wa wex weq 2eu1 pm5.32ri eumo adantl 2moex syl pm4.71i 2eu4