doc-src/HOL/HOL.tex
changeset 43077 7d69154d824b
parent 42673 43766deefc16
child 43270 bc72c1ccc89e
equal deleted inserted replaced
43049:99985426c0bb 43077:7d69154d824b
    65 \subcaption{Binders} 
    65 \subcaption{Binders} 
    66 
    66 
    67 \begin{constants}
    67 \begin{constants}
    68 \index{*"= symbol}
    68 \index{*"= symbol}
    69 \index{&@{\tt\&} symbol}
    69 \index{&@{\tt\&} symbol}
    70 \index{*"| symbol}
    70 \index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working
    71 \index{*"-"-"> symbol}
    71 \index{*"-"-"> symbol}
    72   \it symbol    & \it meta-type & \it priority & \it description \\ 
    72   \it symbol    & \it meta-type & \it priority & \it description \\ 
    73   \sdx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 
    73   \sdx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 
    74         Left 55 & composition ($\circ$) \\
    74         Left 55 & composition ($\circ$) \\
    75   \tt =         & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\
    75   \tt =         & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\