2 ms·
Sorry, I was unclear. I meant that most LCF style theorem provers only have one theorem datatype to carry proof information.
by jojo3000 9y ago
Sorry, I was unclear. I meant that most LCF style theorem provers only have one theorem datatype to carry proof information.