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.
