		Search-engine friendly clone of the ACL2 documentation.
Isodata-implementation
Isodata-macro-definition

Definition of the isodata macro.
Submit the event form generated by isodata-fn.
Macro: isodata
(defmacro isodata
          (&whole call old isomaps &key (predicate 'nil)
                  (undefined ':auto)
                  (new-name ':auto)
                  (new-enable ':auto)
                  (old-to-new-name 'nil
                                   old-to-new-name-suppliedp)
                  (old-to-new-enable 'nil
                                     old-to-new-enable-suppliedp)
                  (new-to-old-name 'nil
                                   new-to-old-name-suppliedp)
                  (new-to-old-enable 'nil
                                     new-to-old-enable-suppliedp)
                  (newp-of-new-name ':auto
                                    newp-of-new-name-suppliedp)
                  (newp-of-new-enable 't
                                      newp-of-new-enable-suppliedp)
                  (verify-guards ':auto)
                  (untranslate ':nice)
                  (hints 'nil)
                  (print ':result)
                  (show-only 'nil)
                  (compatibility 'nil))
 (cons
  'make-event-terse
  (cons
   (cons
    'isodata-fn
    (cons
     (cons 'quote (cons old 'nil))
     (cons
      (cons 'quote (cons isomaps 'nil))
      (cons
       (cons 'quote (cons predicate 'nil))
       (cons
        (cons 'quote (cons undefined 'nil))
        (cons
         (cons 'quote (cons new-name 'nil))
         (cons
          (cons 'quote (cons new-enable 'nil))
          (cons
           (cons 'quote
                 (cons old-to-new-name 'nil))
           (cons
            old-to-new-name-suppliedp
            (cons
             (cons 'quote
                   (cons old-to-new-enable 'nil))
             (cons
              old-to-new-enable-suppliedp
              (cons
               (cons 'quote
                     (cons new-to-old-name 'nil))
               (cons
                new-to-old-name-suppliedp
                (cons
                 (cons 'quote
                       (cons new-to-old-enable 'nil))
                 (cons
                  new-to-old-enable-suppliedp
                  (cons
                   (cons 'quote
                         (cons newp-of-new-name 'nil))
                   (cons
                    newp-of-new-name-suppliedp
                    (cons
                     (cons 'quote
                           (cons newp-of-new-enable 'nil))
                     (cons
                      newp-of-new-enable-suppliedp
                      (cons
                       (cons 'quote (cons verify-guards 'nil))
                       (cons
                        (cons 'quote (cons untranslate 'nil))
                        (cons
                         (cons 'quote (cons hints 'nil))
                         (cons
                          (cons 'quote (cons print 'nil))
                          (cons
                           (cons 'quote (cons show-only 'nil))
                           (cons
                            (cons 'quote (cons compatibility 'nil))
                            (cons
                             (cons 'quote (cons call 'nil))
                             (cons
                              (cons
                               'cons
                               (cons
                                 ''isodata
                                 (cons (cons 'quote (cons old 'nil))
                                       'nil)))
                              '(state))))))))))))))))))))))))))))
   (cons ':suppress-errors
         (cons (not print) 'nil)))))