M. Strecker, M. Luther, F. W. von Henke
Interactive and automated
proof construction in type theory
In: Automated Deduction - A Basis for Applications, W. Bibel und
P. Schmitt, Kluwer Academic Publishers, 1998.
Volume I: Foundations, Chapter 3: Interactive Theorem Proving.
M. Luther, M. Strecker
A guided tour through
Typelab Technical Report UIB-98-03, Universität Ulm, Fakultät für Informatik, Jan. 1998