Removed false statement about /FORBID

[GinoGiotto]

In the help section of the minimizer there is this statement:

2. The use of / FORBID without / ALLOW_NEW_AXIOMS has no effect.

Which is not true, so I removed it.

Example that shows why it's not true:

  $c |- A B $.

  ax-1 $a |- A $.
  ax-2 $a |- A $.

  ${
    hyp.1 $e |- A $.
    hyp.2 $e |- A $.
    inf $a |- B $.
  $}

  th $p |- B $= ax-1 ax-2 inf $.

Metamath - Version 0.199.pre 29-Jan-2022      Type HELP for help, EXIT to exit.
MM> READ test.mm
Reading source file "test.mm"... 161 bytes
161 bytes were read into the source buffer.
The source has 9 statements; 3 are $a and 1 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> PROVE th
Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT th"):
9 th $p |- B $= ... $.
Note:  The proof you are starting with is already complete.
MM-PA> MINIMIZE_WITH * /MAY_GROW
Bytes refer to compressed proof size, steps to uncompressed length.
Scanning forward through statements...
Proof of "th" remained at 3 steps using "ax-1".
Proof of "th" remained at 3 steps using "ax-2".
MM-PA> SHOW NEW_PROOF /NORMAL
Proof of "th":
---------Clip out the proof below this line to put it in the source file:
    ax-2 ax-2 inf $.
---------The proof of "th" (13 bytes) ends above this line.
MM-PA> EXIT
Warning:  You have not saved changes to the proof of "th".
Do you want to EXIT anyway (Y, N) ? Y
Exiting the Proof Assistant.  Type EXIT again to exit Metamath.
MM> PROVE th
Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT th"):
9 th $p |- B $= ... $.
Note:  The proof you are starting with is already complete.
MM-PA> MINIMIZE_WITH * /MAY_GROW /FORBID ax-2
Bytes refer to compressed proof size, steps to uncompressed length.
Scanning forward through statements...
Proof of "th" remained at 3 steps using "ax-1".
MM-PA> SHOW NEW_PROOF /NORMAL
Proof of "th":
---------Clip out the proof below this line to put it in the source file:
    ax-1 ax-1 inf $.
---------The proof of "th" (13 bytes) ends above this line.
MM-PA> EXIT
Warning:  You have not saved changes to the proof of "th".
Do you want to EXIT anyway (Y, N) ? Y
Exiting the Proof Assistant.  Type EXIT again to exit Metamath.
MM>

In the example above I executed the minimizer with and without the /FORBID option, returning two different results. This shows that /FORBID can have some effects even without the /ALLOW_NEW_AXIOMS option.

[tirix]

LGMT

[GinoGiotto]

@digama0 What do you think about this PR?