### 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)`

.