# HG changeset patch
# User wenzelm
# Date 863448445 -7200
# Node ID d2c6f15f38f468631e74729e7ad68429564775e2
# Parent  08e364dfe518dc748718ecc2862c5684f2ac7259
minor tuning;

diff -r 08e364dfe518 -r d2c6f15f38f4 doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Mon May 12 16:46:07 1997 +0200
+++ b/doc-src/Logics/HOL.tex	Mon May 12 16:47:25 1997 +0200
@@ -487,7 +487,7 @@
 \index{*"<"= symbol}
 \begin{tabular}{rrrr} 
   \it symbol    & \it meta-type & \it priority & \it description \\ 
-  \tt ``        & $[\alpha\To\beta ,\alpha\,set]\To  (\beta\,set)$
+  \tt ``        & $[\alpha\To\beta ,\alpha\,set]\To  \beta\,set$
         & Left 90 & image \\
   \sdx{Int}     & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
         & Left 70 & intersection ($\int$) \\