Mark iseradd as discouraged in iset.mm

Use ser3add instead.

Author: jkingdon

iset-discouraged

@@ -235,6 +235,8 @@
 "iseqvalt" is used by "iseqfclt".
 "iseqvalt" is used by "iseqp1t".
 "iser0" is used by "ser0f".
+"iseradd" is used by "fsumadd".
+"iseradd" is used by "ser3add".
 "iserf" is used by "fisumcvg".
 "iserf" is used by "ser0f".
 "isummo" is used by "fisum".
@@ -423,6 +425,7 @@ New usage of "iseqp1t" is discouraged (1 uses).
 New usage of "iseqval" is discouraged (4 uses).
 New usage of "iseqvalt" is discouraged (3 uses).
 New usage of "iser0" is discouraged (1 uses).
+New usage of "iseradd" is discouraged (2 uses).
 New usage of "iserf" is discouraged (2 uses).
 New usage of "isummo" is discouraged (1 uses).
 New usage of "isummolem2" is discouraged (1 uses).

iset.mm

@@ -103881,7 +103881,8 @@ seq K ( .+ , G ) ) $=
     iseradd.4 $e |- ( ( ph /\ k e. ( ZZ>= ` M ) ) ->
                      ( H ` k ) = ( ( F ` k ) + ( G ` k ) ) ) $.
     $( The sum of two infinite series.  (Contributed by NM, 17-Mar-2005.)
-       (Revised by Mario Carneiro, 26-May-2014.) $)
+       (Revised by Mario Carneiro, 26-May-2014.)  Use ~ ser3add instead.
+       (New usage is discouraged.) $)
     iseradd $p |- ( ph -> ( seq M ( + , H , CC ) ` N ) =
         ( ( seq M ( + , F , CC ) ` N ) + ( seq M ( + , G , CC ) ` N ) ) ) $=
       ( vx vy vz caddc cc cv wcel co adantl cvv wa addcl wceq addcom w3a addass

mmil.raw.html

@@ -7060,10 +7060,8 @@
 <TR>
   <TD>seradd</TD>
   <TD>~ ser3add</TD>
-  <TD>iseradd requires that ` F ` , ` G ` , and ` H ` be defined on
-  ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` as in seradd .  This
-  is not a problem when used on infinite sequences, but perhaps this
-  requirement could be relaxed if there is a need.</TD>
+  <TD>The functions ` F ` , ` G ` , and ` H ` need to be defined on
+  ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` .</TD>
 </TR>
 
 <TR>