Definition of the defbyte-ihs-theorems macro.
Macro: defbyte-ihs-theorems
(defmacro defbyte-ihs-theorems (type) (cons 'make-event (cons (cons 'defbyte-ihs-theorems-fn (cons (cons 'quote (cons type 'nil)) '((w state)))) 'nil)))