ACL2-pc::s-prop
(atomic macro)
simplify propositionally
Example:
s-prop
General Form:
(s-prop &rest names)
Simplify, using the default settings for s (which include normalization and rewriting without real backchaining), but with respect to a
theory in which only basic functions and rules (the ones in (theory
'minimal-theory)), together with the names (or parenthesized names) in the
&rest argument names, are enabled.
Also see ACL2-pc::s.
