cbostrum (02/28/83)
I am looking for information on user friendly proof checking systems that encourage a nice style for communicating formal proofs. I am familiar with LCF, AFFIRM and AUTOMATH (this latter is what I think is most appropriate). Oh yes, I am also slightly familiar with the Boyer/Moore stuff. Can anyone out there help me?