Allow in-theory events to be redundant
See redundant-events for discussion of the notion of redundant events.
General Forms: (set-in-theory-redundant-okp nil) ; default (set-in-theory-redundant-okp t) ; allow in-theory events to be redundant
By default, in-theory events are never redundant. This behavior
avoids a redundancy check that could be a bit expensive, as it would require
computing the current theory and checking its equality to the new theory.
Evaluation of the event
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.