# HG changeset patch
# User paulson
# Date 933678354 -7200
# Node ID b009afd1ace55a38aebe4d8eeb4eb3238a2c19c1
# Parent  ac93579530ead9a1fef998110ecb0b84717a8fdd
\underscoreoff needed because of \underscoreon in previous file

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