Skip to content

A utility to enable better support for overriding of syntax notation in Isabelle/HOL, developed by Dr Frank Zeyda.

Notifications You must be signed in to change notification settings

isabelle-utp/Total_Recall

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

11 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Total Recall

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 to no_syntax, but with support for recalling previous changes
  • purge_notation -- similar functionality to no_notation
  • recall_syntax -- used at the beginning of a new theory, recalls previously purged syntax notations

About

A utility to enable better support for overriding of syntax notation in Isabelle/HOL, developed by Dr Frank Zeyda.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published