Major Section: ACL2-BUILT-INS
By default, (read-run-time state) returns (mv runtime state), where
runtime is the elapsed runtime in seconds since the start of the current ACL2
session and state is the resulting ACL2 state. But
read-run-time can be made to return elapsed realtime (wall clock time)
instead; see get-internal-time.
The logical definition probably won't concern many users, but for
completeness, we say a word about it here. That definition uses the function
read-acl2-oracle, which modifies state by popping the value to return
from its acl2-oracle field.
