Hacker News new | ask | show | jobs
by jojo3000 3263 days ago
Sorry, I was unclear. I meant that most LCF style theorem provers only have one theorem datatype to carry proof information.