Table-based alternative to ACL2's named theories.
Rulesets are like theories, but can be extended with additional rules after first being defined. That is, you can build up a ruleset incrementally, across many books, instead of having to define it all at once and having it be forever fixed.
Basic usage of rulesets is just like theories. You can:
When we define a new package
Advanced users can do some nifty things with rulesets, e.g., you can have a superior ruleset that contains other rulesets, and it will grow as you add rules to the contained rulesets.
A ruleset is actually a list of so-called ruleset designators. All ruleset operators, such as e/d* and def-ruleset, take arguments that are rulesets. See expand-ruleset for a discussion of ruleset designators and the corresponding theories that they represent.