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.