doc-src/Logics/CTT.tex
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