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}