minor tuning;

--- 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$) \\