HOL-Theorem-Prover/HOL

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

mn200 opened this issue · 0 comments

mn200 commented

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.