Auto_tac now has type tactic, not unit->tactic

--- a/doc-src/Ref/classical.tex	Fri Jan 02 11:17:06 1998 +0100
+++ b/doc-src/Ref/classical.tex	Fri Jan 02 11:59:06 1998 +0100
@@ -37,7 +37,7 @@
 set theory.  To attempt to prove \emph{all} subgoals using a combination of
 rewriting and classical reasoning, try
 \begin{ttbox}
-by (Auto_tac());
+by Auto_tac;
 \end{ttbox}
 To do all obvious logical steps, even if they do not prove the
 subgoal, type one of the following:
@@ -467,7 +467,7 @@
 the default claset and simpset (see \S\ref{sec:current-claset} below).  For
 interactive use, the shorthand \texttt{auto();} abbreviates 
 \begin{ttbox}
-by (Auto_tac());
+by Auto_tac;
 \end{ttbox}
 
 \subsection{Other classical tactics}
@@ -566,7 +566,7 @@
 tactics
 \begin{ttbox}
 Blast_tac        : int -> tactic
-Auto_tac         : unit -> tactic
+Auto_tac         :        tactic
 Fast_tac         : int -> tactic
 Best_tac         : int -> tactic
 Deepen_tac       : int -> int -> tactic