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.

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.