ACL2-PC::SL

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


Examples:
sl
(sl 3)


General Form:
(sl &optional backchain-limit)
Simplify, but with all function definitions disabled (see function-theory in the top-level ACL2 loop), except for a few basic functions (the ones in *s-prop-theory*). If backchain-limit is supplied and not nil, then it should be a nonnegative integer; see (help s).