Major Section: EVENTS
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
When this flag is set to
t, subterms that occur multiple times
in a clause are abstracted away with
let*, generally shortening
the displayed size of the clauses. This flag only affects how
clauses are printed. It does not change what terms the theorem
:set-let*-abstractionp twill cause the prettyprinter to do ``let* abstraction'' on clauses before they are printed. The algorithm finds the maximal multiply-occuring subterm and extracts it, binding it to some new variable and replacing its occurrences by that variable. This produces a
let*form. This process is iterated until no subterm occurs more than once. This process generally takes a little time, but less time than to print large clauses. The process can greatly reduce the amount of text produced by the prover.
THIS ONLY AFFECTS HOW THE CLAUSES ARE PRINTED! The unabstracted clauses are manipulated by the theorem prover.
:set-let*-abstractionp nilrestores normal clause printing.
The mode is stored in the defaults table, See acl2-defaults-table.
Thus, the mode may be set locally in books.