dynamic-e-d

(defun get-current-dynamic-theory
  (pspv world)
  (declare (xargs :mode :program))
  (let* ((ens (access rewrite-constant
         (access prove-spec-var pspv :rewrite-constant)
         :current-enabled-structure)) (ens-index (access enabled-structure ens :index-of-last-enabling)))
    (if (equal ens-index (+ -1 (get-next-nume world)))
      (strip-cdrs (cdr (access enabled-structure ens :theory-array)))
      (current-theory-fn :here world))))

(defun dynamic-e/d
  (e/d keyword-alist pspv world)
  (declare (xargs :mode :program))
  (let ((enable (car e/d)) (disable (cadr e/d)))
    (let* ((old-theory (get-current-dynamic-theory pspv world)) (new-theory (set-difference-equal (append enable old-theory) disable)))
      (if (member-equal :in-theory keyword-alist)
        (observation-cw 'dynamic-e/d
          "It is not yet clear how dynamic-e/d should ~
                           interact with user supplied :in-theory hints.  So, ~
                           dynamic-e/d does not interfere with the user's ~
                           hint.")
        (let ((new-keyword-alist (splice-keyword-alist :dynamic-e/d `(:in-theory ',NEW-THEORY)
               keyword-alist)))
          new-keyword-alist)))))