HOL
HOL copied to clipboard
Store location information about where theorems were proved in Theory.sig files
The modern syntax could stash line-number information for theorems that could in turn be put into comments in the xTheory.sig file for possible reference by tools (or even dedicated humans).
Thanks to Kacper Korban for the idea.