--- 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)$ &
--- 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}
--- 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}