diff -r ac93579530ea -r b009afd1ace5 doc-src/Logics/CTT.tex
--- 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