|
|
|---|
|
|
|
|---|
Prove a theorem using GL symbolic simulation, but don't store it, like with thm.
Exactly the same as def-gl-thm, but does not store the resulting theorem: def-gl-thm is to gl-thm as defthm is to thm. The :rule-classes argument is accepted, but ignored.