Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Removed false statement about /FORBID #154

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Removed false statement about /FORBID #154

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions src/mmhlpb.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1293,11 +1293,10 @@ H(" statement matching <label-match>. This is useful for avoiding");
H(" the use of undesired axioms when reducing proof length. For");
H(" example, MINIMIZE_WITH ... / FORBID ax-ac,ax-inf* will not shorten");
H(" the proof with any statement that depends on ax-ac, ax-inf, or");
H(" ax-inf2 (in the set.mm as of this writing). Notes: 1. / FORBID");
H(" can be less useful than / NO_NEW_AXIOMS_FROM because it will");
H(" also suppress trying statements that depend on <label-list> axioms");
H(" already used by the proof. / FORBID may become deprecated. 2. The");
H(" use of / FORBID without / ALLOW_NEW_AXIOMS has no effect.");
H(" ax-inf2 (in the set.mm as of this writing). Note: / FORBID can be");
H(" less useful than / NO_NEW_AXIOMS_FROM because it will also suppress");
H(" trying statements that depend on <label-list> axioms already used");
H(" by the proof. / FORBID may become deprecated.");
H(" / OVERRIDE - By default, MINIMIZE_WITH skips statements that have");
H(" \"(New usage is discouraged.)\" in their description comment.");
H(" With this qualifier it will try to use them anyway.");
Expand Down