Generate the
(isodata-gen-old-to-new-thm appcond-thm-names old$ arg-isomaps res-isomaps new$ old-to-new$ old-to-new-enable$ new-to-old$ old-to-new-lemma-name old-to-list-of-mv-nth-name wrld) → (mv old-to-new-local-event old-to-new-exported-event)
Function:
(defun isodata-gen-old-to-new-thm (appcond-thm-names old$ arg-isomaps res-isomaps new$ old-to-new$ old-to-new-enable$ new-to-old$ old-to-new-lemma-name old-to-list-of-mv-nth-name wrld) (declare (xargs :guard (and (symbol-symbol-alistp appcond-thm-names) (symbolp old$) (isodata-symbol-isomap-alistp arg-isomaps) (isodata-pos-isomap-alistp res-isomaps) (symbolp new$) (symbolp old-to-new$) (booleanp old-to-new-enable$) (symbolp new-to-old$) (symbolp old-to-new-lemma-name) (symbolp old-to-list-of-mv-nth-name) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-old-to-new-thm)) (declare (ignorable __function__)) (b* ((formula (isodata-gen-old-to-new-thm-formula old$ arg-isomaps res-isomaps new$ wrld)) (formula (untranslate formula t wrld)) (hints (isodata-gen-old-to-new-thm-hints appcond-thm-names old$ arg-isomaps res-isomaps new-to-old$ old-to-new-lemma-name old-to-list-of-mv-nth-name wrld))) (evmac-generate-defthm old-to-new$ :formula formula :hints hints :enable old-to-new-enable$))))