Definition of the defthm-inst macro.
Macro:
(defmacro defthm-inst (thm sothminst &rest options) (cons 'make-event-terse (cons (cons 'defthm-inst-fn (cons (cons 'quote (cons thm 'nil)) (cons (cons 'quote (cons sothminst 'nil)) (cons (cons 'quote (cons options 'nil)) (cons (cons 'cons (cons ''defthm-inst (cons (cons 'quote (cons thm 'nil)) 'nil))) '(state)))))) 'nil)))
Macro:
(defmacro acl2::defthm-inst (&rest args) (cons 'defthm-inst args))