Indexing of Zermelo-Fraenkel

[andrejbauer]

I'd be very happy if someone can explain to me why "Zermelo-Fraenkel", "ZF" and "ZFC" refuse to appear in the index.

[DanGrayson]

In the log file for makeindex, called hott-online.ilg, we error messages about those:

!! Input index error (file = hott-online.idx, line = 59):
   -- Extra `!' at position 61 of first argument.
!! Input index error (file = hott-online.idx, line = 60):
   -- Extra `!' at position 36 of first argument.
!! Input index error (file = hott-online.idx, line = 61):
   -- Extra `!' at position 37 of first argument.

The three lines in question come from hott-online.idx and are:

\indexentry{Zermelo-Fraenkel set theory|hyperindexformat{\see{set theory!Zermelo-Fraenkel}}}{6}
\indexentry{ZF|hyperindexformat{\see{set theory!Zermelo-Fraenkel}}}{6}
\indexentry{ZFC|hyperindexformat{\see{set theory!Zermelo-Fraenkel}}}{6}

The problem is the exclamation points.

The fix is

--- a/introduction.tex
+++ b/introduction.tex
@@ -184,9 +184,9 @@ such as the recent formalization of the  Feit-Thompson odd-order theorem in \Coq

 But the traditional view is that mathematics is founded on set theory, in the sense that all mathematical objects and constructions can be coded into a theory such as Zermelo--Fraenkel set theory (ZF).
 \index{set theory!Zermelo-Fraenkel}%
-\indexsee{Zermelo-Fraenkel set theory}{set theory!Zermelo-Fraenkel}%
-\indexsee{ZF}{set theory!Zermelo-Fraenkel}%
-\indexsee{ZFC}{set theory!Zermelo-Fraenkel}%
+\indexsee{Zermelo-Fraenkel set theory}{set theory}%
+\indexsee{ZF}{set theory}%
+\indexsee{ZFC}{set theory}%
 However, it is well-established by now that for most mathematics outside of set theory proper, the intricate hierarchical membership structure of sets in ZF is really unnecessary: a more ``structural'' theory, such as Lawvere's Elementary Theory of the Category of Sets~\cite{lawvere:etcs-long}, suffices.
 \index{Elementary Theory of the Category of Sets}%

, which I've checked in at 70f668ffb31a6ccb302967b6eac23370a44afc84

[mikeshulman]

Ah, I was fixing this at the same time. This keeps biting me as well.