regenerate the tau data base relative to the current enabled theory
Major Section:  EVENTS


General Form:
(regenerate-tau-data-base :doc doc-string)
where doc-string is an optional documentation string not beginning with ``:Doc-Section ...''.

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 regenerate-tau-data-base event, there is no way we can store the documentation string doc-string in our il[documentation] data base. Hence, we actually prohibit doc-string from having the form of an ACL2 documentation string; see doc-string.

See tau-system.