It does. And if classical logic is what they like, they can use Isabelle/HOL just as nicely. It is classical. It has wonderful automation. Kevin gets attention because he is bold, not because he is correct.
Anonymous comments are cowardly; please show yourself. If you stay anonymous I am not aware of power dynamics, and I cannot adjust my response accordingly.
Anonymous comments are cowardly; please show yourself. If you stay anonymous I am not aware of power dynamics, and I cannot adjust my response accordingly.