|
|
|---|
|
|
|
|---|
Prove a theorem using GL symbolic simulation with parametrized case-splitting, without storing the theorem.
Exactly the same as def-gl-param-thm, but does not store the resulting theorem: def-gl-param-thm is to gl-param-thm as defthm is to thm. The :rule-classes argument is accepted, but ignored.