Hons-wash!
A version of hons-wash for parallel execution
This function is only of interest to ACL2(p) users; see parallelism, because for ACL2 it suffices to use hons-wash. However,
if parallel execution is enabled (see set-parallel-execution), as it is
by default in ACL2(p), then hons-wash may be a no-op (other than to print
a warning), in order to avoid thread-unsafe behavior. If you are not
concerned about thread safety, for example when you want to call
hons-wash directly in the top-level loop, you can use hons-wash!,
which does not check for parallelism violations. However, hons-wash!
requires a trust tag; see defttag.
