		Search-engine friendly clone of the ACL2 documentation.

Rulesets

Def-ruleset

(def-ruleset name form) creates a new ruleset.

Examples:

(def-ruleset my-rules
  '(append reverse))

(def-ruleset other-rules
  '(member-equal my-rules revappend))

The first example creates a new ruleset, my-rules, with only the definitions of append and reverse.

The section example creates a new ruleset, other-rules, with the definitions of member-equal and revappend, and also a link to my-rules. When rules are added to my-rules, other-rules also grows.

See def-ruleset! for a version that's more friendly towards redundant calls.