Preface
A Compendium of Continuous Lattices in MIZAR
A Proof of GMP Square Root
Automated Proof Construction in Type Theory Using Resolution*
Proof Reflection in Coq
External Rewriting for Skeptical Proof Assistants
Algorithms and Proofs Inheritance in the FOC Language
A New Implementation of Automath
A Comparison of Mizar and Isar
Author Index to Volume 29
Subject Index to Volume 29
Contents to Volume 29