To shorten many prettyprinted clauses
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. Moreover, its effect is to set the ACL2-defaults-table, and hence its effect is local to the book or encapsulate form containing it; see ACL2-defaults-table.
When this flag is set to
:set-let*-abstractionp t ;;; or, (set-let*-abstractionp t)
will cause the prettyprinter to do ``let* abstraction'' on clauses before
they are printed. The algorithm finds the maximal multiply-occurring subterm
and extracts it, binding it to some new variable and replacing its occurrences
by that variable. This produces a
THIS ONLY AFFECTS HOW THE CLAUSES ARE PRINTED! The unabstracted clauses are manipulated by the theorem prover.
restores normal clause printing.
The mode is stored in the defaults table, See ACL2-defaults-table. Thus, the mode may be set locally in books.