DEFAULT-TOTAL-PARALLELISM-WORK-LIMIT

for ACL2(p): returns the default value for global total-parallelism-work-limit
Major Section:  PARALLEL-PROOF

See set-total-parallelism-work-limit.