control warnings
Major Section:  EVENTS

(set-inhibit-warnings "theory" "use")
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. Moreover, its effect is to set the acl2-defaults-table, and hence its effect is local to the book or encapsulate form containing it; see acl2-defaults-table.

General Form:
(set-inhibit-warnings string1 string2 ...)
where each string is considered without regard to case. This macro is equivalent to (table acl2-defaults-table :inhibit-warnings lst), where lst is the list of strings supplied. This macro is an event (see table), but no output results from a set-inhibit-warnings event.

The effect of this event is to suppress any warning whose label is a member of this list (where again, case is ignored). For example, the warning

  ACL2 Warning [Use] in ( THM ...):  It is unusual to :USE ....
will not be printed if "use" (or "USE", etc.) is a member of the given list of strings.

Of course, if warnings are inhibited overall -- see set-inhibit-output-lst -- then the value of :inhibit-warnings is entirely irrelevant.