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.