# 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}