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}