It's not entirely clear to me what #2(Tag.dest_tag(Thm.tag th)) is supposed to say about th, but if it's supposed to say something like "the axioms that this theorem's proof depended on", then exporting to dat and reloading with DISK_THM oracle destroys this information.
I'm opening this issue to get clarity on whether it's a bug that the axioms aren't retained, and to record them for disk thms if so.
It's not entirely clear to me what
#2(Tag.dest_tag(Thm.tag th))is supposed to say aboutth, but if it's supposed to say something like "the axioms that this theorem's proof depended on", then exporting todatand reloading withDISK_THMoracle destroys this information.I'm opening this issue to get clarity on whether it's a bug that the axioms aren't retained, and to record them for disk thms if so.