top

advise case-splitting-rules cws dead-events defevaluator-fast def-functional-instance defined-const define-keyed-function defmacfun defsum defthmg deftuple do-not easy-simplify equality-with-hons-copy er-soft-logic fake-event flag include-an-arithmetic-book include-raw k-induction last-theory-change lint match-tree memoize-prover-fns mv-nth names-after nld open-trace-file-bang oracle-eval oracle-eval-real oracle-timelimit oracle-time pattern-match plev-ccl plev doc prove-dollar removable-runes remove-hyps rewrite-dollar-book rewrite-dollar rewrite-with-equality rulesets run-script safe-case saved-errors save-obligs some-events stobj-frame symlet table-replay templates theory-tools time-dollar-with-gc trivial-ancestors-check types-misc untranslate-for-exec with-arith1-help with-arith5-help with-arith-help without-subsumption with-quoted-forms with-supporters-doc with-supporters elide-event-doc elide-event eval-events-from-file eval-events-from-file-doc