A version of defthm with testing disabled.
A macro that locally turns off cgen testing and then calls defthm.
