When trying to copy a form into my ACL2 shell buffer using ctrl+t e, and I've already placed a time$ in my shell buffer, I get an error about not being able to paste the form. How do I change the emacs macro so that I can paste into ACL2 shell buffers that already have (time$ written into them?
Place this at the end of your ~/.emacs file:
(setq *acl2-insert-pats* '(:not ".*%[ ]*$" "[^(]*$[ ]*$" "^$"))