changeset 7159 | b009afd1ace5 |
parent 6170 | 9a59cf8ae9b5 |
child 9695 | ec7d7f877712 |
--- a/doc-src/Logics/CTT.tex Tue Aug 03 13:05:13 1999 +0200 +++ b/doc-src/Logics/CTT.tex Tue Aug 03 13:05:54 1999 +0200 @@ -2,6 +2,8 @@ \chapter{Constructive Type Theory} \index{Constructive Type Theory|(} +\underscoreoff %this file contains _ in rule names + Martin-L\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can be viewed at many different levels. It is a formal system that embodies the principles of intuitionistic mathematics; it embodies the