BJ's Review remarks

set.mm

@@ -68489,7 +68489,7 @@ result of an operator (deduction version).  (Contributed by Paul
 
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
-  Convert operation laws using setvar variables to class notation
+  Variable-to-class conversion for operations
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
 $)
 
@@ -180550,7 +180550,7 @@ obviously not a bijection (by Cantor's theorem ~ canth2 ), and in fact
       BVCVENQUPNVFOVGVHVIVJVK $.
   $}
 
-  $( Obsolete proof of ~ gcdmultiple as of 12-Jan-2024.  Extend ~ gcdmultiple
+  $( Obsolete proof of ~ gcdmultiplez as of 12-Jan-2024.  Extend ~ gcdmultiple
      so ` N ` can be an integer.  (Contributed by Scott Fenton, 18-Apr-2014.)
      (Revised by Mario Carneiro, 19-Apr-2014.)  (New usage is discouraged.)
      (Proof modification is discouraged.) $)