diff -r 99985426c0bb -r 7d69154d824b doc-src/ZF/FOL.tex --- a/doc-src/ZF/FOL.tex Mon May 30 15:30:05 2011 +0100 +++ b/doc-src/ZF/FOL.tex Mon May 30 16:10:12 2011 +0100 @@ -77,7 +77,7 @@ \begin{center} \index{*"= symbol} \index{&@{\tt\&} symbol} -\index{*"| symbol} +\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working \index{*"-"-"> symbol} \index{*"<"-"> symbol} \begin{tabular}{rrrr}