Coq & ProofWeb

在ProofWeb的主页http://prover.cs.ru.nl点击按钮 ,然后在Select a saved file to load:中选择tarski-hg.v,然后在下面的下拉框中选择Coq,点 ,就可以看到Tarski’s Fixed Point Theorem的形式化证明过程,这个证明过程可以作为Coq和ProofWeb的一个不错的demo。