HOL icon indicating copy to clipboard operation
HOL copied to clipboard
verified publisher icon HOL-Theorem-Prover

Consider using OpenTheory for persistent theories

Open xrchz opened this issue 13 years ago • 2 comments

See discussion on #71. Could also be useful alongside DISK_THM-style persistent theories.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

xrchz avatar Aug 07 '12 10:08 xrchz

Is this done given that we now have otknl?

xrchz avatar Aug 07 '25 11:08 xrchz

I don't think so. I assume the original suggestion was to store open-theory proofs as permanent records of theorems. In contrast, the otknl approach generates open-theory proofs as build products.

mn200 avatar Aug 08 '25 00:08 mn200