# HG changeset patch
# User paulson
# Date 1306768537 -3600
# Node ID e2631aaf1e1e5ba3fefa446feb8f23b5a2f7c401
# Parent  7b06cd71792cf495ea32f22c6d7db6334026432f# Parent  7d69154d824bb01e21fcbdeedd3ad68ec612cafb
merged

diff -r 7b06cd71792c -r e2631aaf1e1e doc-src/HOL/HOL.tex
--- a/doc-src/HOL/HOL.tex	Mon May 30 17:07:48 2011 +0200
+++ b/doc-src/HOL/HOL.tex	Mon May 30 16:15:37 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 7b06cd71792c -r e2631aaf1e1e doc-src/Intro/getting.tex
--- a/doc-src/Intro/getting.tex	Mon May 30 17:07:48 2011 +0200
+++ b/doc-src/Intro/getting.tex	Mon May 30 16:15:37 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 7b06cd71792c -r e2631aaf1e1e doc-src/ZF/FOL.tex
--- a/doc-src/ZF/FOL.tex	Mon May 30 17:07:48 2011 +0200
+++ b/doc-src/ZF/FOL.tex	Mon May 30 16:15:37 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}