diff -r 99985426c0bb -r 7d69154d824b doc-src/Intro/getting.tex
--- a/doc-src/Intro/getting.tex	Mon May 30 15:30:05 2011 +0100
+++ b/doc-src/Intro/getting.tex	Mon May 30 16:10:12 2011 +0100
@@ -119,7 +119,11 @@
 are just terms of type~\texttt{prop}.  
 \index{meta-implication}
 \index{meta-quantifiers}\index{meta-equality}
-\index{*"!"! symbol}\index{*"["| symbol}\index{*"|"] symbol}
+\index{*"!"! symbol}
+
+\index{["!@{\tt[\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working
+\index{"!]@{\tt\char124]} symbol} % so these are [| and |]
+
 \index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
 \[\dquotes
   \begin{array}{l@{\quad}l@{\quad}l}