HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Store location information about where theorems were proved in Theory.sig files

Open mn200 opened this issue 2 years ago • 0 comments

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.

mn200 avatar Feb 14 '23 09:02 mn200