merged
authorpaulson
Mon May 30 16:15:37 2011 +0100 (2011-05-30)
changeset 43078e2631aaf1e1e
parent 43076 7b06cd71792c
parent 43077 7d69154d824b
child 43079 4022892a2f28
merged
     1.1 --- a/doc-src/HOL/HOL.tex	Mon May 30 17:07:48 2011 +0200
     1.2 +++ b/doc-src/HOL/HOL.tex	Mon May 30 16:15:37 2011 +0100
     1.3 @@ -67,7 +67,7 @@
     1.4  \begin{constants}
     1.5  \index{*"= symbol}
     1.6  \index{&@{\tt\&} symbol}
     1.7 -\index{*"| symbol}
     1.8 +\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working
     1.9  \index{*"-"-"> symbol}
    1.10    \it symbol    & \it meta-type & \it priority & \it description \\ 
    1.11    \sdx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 
     2.1 --- a/doc-src/Intro/getting.tex	Mon May 30 17:07:48 2011 +0200
     2.2 +++ b/doc-src/Intro/getting.tex	Mon May 30 16:15:37 2011 +0100
     2.3 @@ -119,7 +119,11 @@
     2.4  are just terms of type~\texttt{prop}.  
     2.5  \index{meta-implication}
     2.6  \index{meta-quantifiers}\index{meta-equality}
     2.7 -\index{*"!"! symbol}\index{*"["| symbol}\index{*"|"] symbol}
     2.8 +\index{*"!"! symbol}
     2.9 +
    2.10 +\index{["!@{\tt[\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working
    2.11 +\index{"!]@{\tt\char124]} symbol} % so these are [| and |]
    2.12 +
    2.13  \index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
    2.14  \[\dquotes
    2.15    \begin{array}{l@{\quad}l@{\quad}l}
     3.1 --- a/doc-src/ZF/FOL.tex	Mon May 30 17:07:48 2011 +0200
     3.2 +++ b/doc-src/ZF/FOL.tex	Mon May 30 16:15:37 2011 +0100
     3.3 @@ -77,7 +77,7 @@
     3.4  \begin{center}
     3.5  \index{*"= symbol}
     3.6  \index{&@{\tt\&} symbol}
     3.7 -\index{*"| symbol}
     3.8 +\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working
     3.9  \index{*"-"-"> symbol}
    3.10  \index{*"<"-"> symbol}
    3.11  \begin{tabular}{rrrr}