# HG changeset patch # User paulson # Date 1306765805 -3600 # Node ID 99985426c0bb9bd5eaa121f3bd209d1c8d69f91c # Parent c62bed03fbce3cd70992bc6614c50d6656345ece Workaround for hyperref bug affecting index entries involving the | symbol diff -r c62bed03fbce -r 99985426c0bb doc-src/Logics/CTT.tex --- a/doc-src/Logics/CTT.tex Mon May 30 13:58:00 2011 +0200 +++ b/doc-src/Logics/CTT.tex Mon May 30 15:30:05 2011 +0100 @@ -644,10 +644,14 @@ \begin{figure} \index{#+@{\tt\#+} symbol} \index{*"- symbol} -\index{"|"-@{{\tt"|"-"|} symbol}} \index{#*@{\tt\#*} symbol} \index{*div symbol} \index{*mod symbol} + +\index{absolute difference} +\index{"!-"!@{\tt\char124-\char124} symbol} +%\char124 is vertical bar. We use ! because | stopped working + \begin{constants} \it symbol & \it meta-type & \it priority & \it description \\ \tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\ diff -r c62bed03fbce -r 99985426c0bb doc-src/Logics/LK.tex --- 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}