This is utility to enable better support for overriding of syntax notation in Isabelle/HOL, developed by Dr Frank Zeyda. In Isabelle, one can remove previously added syntax notation using command like no_syntax and no_notation. However, these notational changes are not preserved by the theory import mechanism, and so conflicts can arise.
For example, let's say I'd like to remove some syntax defined in theory Main. I can do that using no_notation in another theory A that imports Main. But then let's say I have a other theory B that imports both A and a further thory C (a library, for example) that also imports Main. In this case, the overriden syntax would not be preserved, and syntax ambiguity errors arise.
The Total Recall utility overcomes this situation by allowing previously overriden syntax to be totally recalled (hence the name). There are three new commands:
purge_syntax-- corresponds tono_syntax, but with support for recalling previous changespurge_notation-- similar functionality tono_notationrecall_syntax-- used at the beginning of a new theory, recalls previously purged syntax notations