Major Section: EVENTS
Example: (regenerate-tau-data-base) General Form: (regenerate-tau-data-base :doc doc-string)where
doc-stringis an optional documentation string not beginning with ``
The tau data base is regenerated by scanning the current logical world and re-processing every event in it relative to the current enabled theory and current tau auto mode settings.
BECAUSE NO UNIQUE name is associated with a
there is no way we can store the documentation string
in our il[documentation] data base. Hence, we actually prohibit
from having the form of an ACL2 documentation string;