		Search-engine friendly clone of the ACL2 documentation.

Rulesets

E/d*

Ruleset-aware version of e/d.

Examples:

(in-theory (e/d* (unusual-rules append)
                 (expensive-rules default-car default-cdr)))

(defthm ...
   :hints (("Goal"
            :in-theory (e/d* (unusual-rules append)
                             (expensive-rules default-car
                              default-cdr)))))

Definitions and Theorems

Function: e/d*-fn

(defun e/d*-fn (theory e/d-list enable-p)
 (declare (xargs :guard (and (true-list-listp e/d-list)
                             (or (eq enable-p t)
                                 (eq enable-p nil)))))
 (cond
  ((atom e/d-list) theory)
  (enable-p
   (e/d*-fn
    (cons
     'union-theories
     (cons
          theory
          (cons (cons 'expand-ruleset
                      (cons (cons 'quote (cons (car e/d-list) 'nil))
                            '(world)))
                'nil)))
    (cdr e/d-list)
    nil))
  (t
   (e/d*-fn
    (cons
     'set-difference-theories
     (cons
          theory
          (cons (cons 'expand-ruleset
                      (cons (cons 'quote (cons (car e/d-list) 'nil))
                            '(world)))
                'nil)))
    (cdr e/d-list)
    t))))