# HG changeset patch # User paulson # Date 1306768212 -3600 # Node ID 7d69154d824bb01e21fcbdeedd3ad68ec612cafb # Parent 99985426c0bb9bd5eaa121f3bd209d1c8d69f91c Workaround for bug involving makeindex, hyperref and the | symbol diff -r 99985426c0bb -r 7d69154d824b doc-src/HOL/HOL.tex --- a/doc-src/HOL/HOL.tex Mon May 30 15:30:05 2011 +0100 +++ b/doc-src/HOL/HOL.tex Mon May 30 16:10:12 2011 +0100 @@ -67,7 +67,7 @@ \begin{constants} \index{*"= symbol} \index{&@{\tt\&} symbol} -\index{*"| symbol} +\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working \index{*"-"-"> symbol} \it symbol & \it meta-type & \it priority & \it description \\ \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 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} diff -r 99985426c0bb -r 7d69154d824b doc-src/ZF/FOL.tex --- a/doc-src/ZF/FOL.tex Mon May 30 15:30:05 2011 +0100 +++ b/doc-src/ZF/FOL.tex Mon May 30 16:10:12 2011 +0100 @@ -77,7 +77,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}