doc-src/Logics/LK.tex
changeset 43049 99985426c0bb
parent 42637 381fdcab0f36
--- a/doc-src/Logics/LK.tex	Mon May 30 13:58:00 2011 +0200
+++ b/doc-src/Logics/LK.tex	Mon May 30 15:30:05 2011 +0100
@@ -59,7 +59,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}