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.
This event sets the default backchain-limit used when a new 
rewrite or linear rule is admitted.  It must be nil or a
non-negative integer.  (See backchain-limit for details.)
:set-default-backchain-limit nil ; do not impose additional limits
:set-default-backchain-limit 0   ; allow only type-reasoning for
                                 ; relieving hypotheses
:set-default-backchain-limit 500 ; allow backchaining to a depth of
                                 ; no more than 500