Mark iisum as discouraged in iset.mm

Use isum instead.

Author: jkingdon

iset-discouraged

@@ -160,6 +160,9 @@
 "hbs1" is used by "mopick".
 "hbs1" is used by "nfs1v".
 "hbs1" is used by "sb9v".
+"iisum" is used by "isum".
+"iisum" is used by "isumclim".
+"iisum" is used by "isumclim3".
 "iseq1" is used by "iseqcaopr3".
 "iseq1" is used by "iseqcoll".
 "iseq1" is used by "iseqfveq".
@@ -383,6 +386,7 @@ New usage of "fisumser" is discouraged (2 uses).
 New usage of "fnexALT" is discouraged (0 uses).
 New usage of "hbs1" is discouraged (5 uses).
 New usage of "idALT" is discouraged (0 uses).
+New usage of "iisum" is discouraged (3 uses).
 New usage of "iseq1" is discouraged (7 uses).
 New usage of "iseq1t" is discouraged (1 uses).
 New usage of "iseqcaopr" is discouraged (1 uses).

iset.mm

@@ -115524,7 +115524,8 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
       iisum.4 $e |- ( ( ph /\ k e. Z ) -> B e. CC ) $.
       $( Series sum with an upper integer index set (i.e. an infinite series).
          (Contributed by Mario Carneiro, 15-Jul-2013.)  (Revised by Mario
-         Carneiro, 7-Apr-2014.) $)
+         Carneiro, 7-Apr-2014.)  Use ~ isum instead.
+         (New usage is discouraged.) $)
       iisum $p |- ( ph -> sum_ k e. Z B = ( ~~> ` seq M ( + , F , CC ) ) ) $=
         ( vx ssidd cv wcel wa cfv cc0 cif simpr iftrued eqtr4d wdc wn orc df-dc
         wo sylibr adantl ralrimiva zisum ) AKFBCDEFGHAFLACMZFNZOZUKDPBULBQRIUMU