Major Section: PROOF-CHECKER-COMMANDS
Example: s-propSimplify, using the default settings for
General Form: (s-prop &rest names)
s(which include if-normalization and rewriting without real backchaining), but with respect to a theory in which only basic functions and rules (the ones in
*s-prop-theory*), together with the names (or parenthesized names) in the
names, are enabled.
See also the documentation for