Definition/store_thm/etc to collect position metadata from location pragmas

[oskarabrahamsson]

This would allow editor modes (and humans) to find this information about theorems and constants using e.g. DB.find or the upcoming Defnbase functionality.

[oskarabrahamsson]

I don't know if it's possible for HOL to deduce the true path of a theory's source file from the name of the theory, but if it isn't, then perhaps the location pragmas could be augmented to optionally carry a filename.