Macro that can be used to create event names by concatenating strings, symbols, numbers, and characters.
Macro: mk-name
(defmacro mk-name (&rest x) (cons 'acl2::packn-pos (cons (cons 'list x) '('mk-name))))
