Query or set tau system status
Examples: (tau-status) (tau-status :system t) (tau-status :auto-mode nil) (tau-status :system t :auto-mode nil) General Form: (tau-status :system a :auto-mode b)
The two flags are independent. For example, the tau system may be disabled in proof attempts even though it is automatically (and silently) extending its database as rules of other classes are added.
Flag (a) is actually toggled by enabling or disabling the
This macro expands into zero, one, or two events, as required by the
supplied values of flags
If no arguments are supplied the form is not an event and simply returns
(as an error-triple,
ACL2 !>(tau-system) ((:SYSTEM NIL) (:AUTO-MODE T))
intended to be self-explanatory.