ACL2-PC::S-PROP

(atomic macro) simplify propositionally
Major Section:  PROOF-CHECKER-COMMANDS

Example:
s-prop

General Form: (s-prop &rest names)

Simplify, using the default settings for 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 &rest argument names, are enabled.

See also the documentation for s.