Hons-clear!
A version of hons-clear for parallel execution
This function is only of interest to ACL2(p) users; see parallelism, because for ACL2 it suffices to use hons-clear.
However, if parallel execution is enabled (see set-parallel-execution),
as it is by default in ACL2(p), then hons-clear 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-clear directly in the top-level loop, you can use hons-clear!,
which does not check for parallelism violations. However, hons-clear!
requires a trust tag; see defttag.