### 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 `(theory 'minimal-theory)`

). The
`backchain-limit`

has a default of 0, but if is supplied and
not `nil`

, then it should be a nonnegative integer; see the
documentation for `s`

.
WARNING: This command completely ignores `in-theory`

commands that are
executed inside the proof-checker.