1.1 --- a/doc-src/Ref/classical.tex	Tue Jan 18 11:00:10 2000 +0100
     1.2 +++ b/doc-src/Ref/classical.tex	Tue Jan 18 11:33:31 2000 +0100
     1.3 @@ -240,21 +240,21 @@
     1.4  supports the following operations (provided the classical reasoner is
     1.5  installed!):
     1.6  \begin{ttbox} 
     1.7 -empty_cs    : claset
     1.8 -print_cs    : claset -> unit
     1.9 -rep_cs      : claset -> {safeEs: thm list, safeIs: thm list,
    1.10 -                         hazEs: thm list,  hazIs: thm list, 
    1.11 -                         swrappers: (string * wrapper) list, 
    1.12 -                         uwrappers: (string * wrapper) list,
    1.13 -                         safe0_netpair: netpair, safep_netpair: netpair,
    1.14 -                           haz_netpair: netpair,   dup_netpair: netpair}
    1.15 -addSIs      : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.16 -addSEs      : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.17 -addSDs      : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.18 -addIs       : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.19 -addEs       : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.20 -addDs       : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.21 -delrules    : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.22 +empty_cs : claset
    1.23 +print_cs : claset -> unit
    1.24 +rep_cs : claset -> \{safeEs: thm list, safeIs: thm list,
    1.25 +                    hazEs: thm list,  hazIs: thm list, 
    1.26 +                    swrappers: (string * wrapper) list, 
    1.27 +                    uwrappers: (string * wrapper) list,
    1.28 +                    safe0_netpair: netpair, safep_netpair: netpair,
    1.29 +                    haz_netpair: netpair, dup_netpair: netpair\}
    1.30 +addSIs   : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.31 +addSEs   : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.32 +addSDs   : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.33 +addIs    : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.34 +addEs    : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.35 +addDs    : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.36 +delrules : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.37  \end{ttbox}
    1.38  The add operations ignore any rule already present in the claset with the same
    1.39  classification (such as Safe Introduction).  They print a warning if the rule
    1.40 @@ -451,9 +451,10 @@
    1.41      rangeI} in {\HOL} and \texttt{RepFunI} in {\ZF}.  There are often
    1.42      alternatives to such rules, for example {\tt
    1.43      range_eqI} and \texttt{RepFun_eqI}.
    1.44 -\item The message {\small\tt Function Var's argument not a bound variable\ }
    1.45 -relates to the lack of higher-order unification.  Function variables
    1.46 -may only be applied to parameters of the subgoal.
    1.47 +\item Function variables may only be applied to parameters of the subgoal.
    1.48 +(This restriction arises because the prover does not use higher-order
    1.49 +unification.)  If other function variables are present then the prover will
    1.50 +fail with the message {\small\tt Function Var's argument not a bound variable}.
    1.51  \item Its proof strategy is more general than \texttt{fast_tac}'s but can be
    1.52    slower.  If \texttt{blast_tac} fails or seems to be running forever, try {\tt
    1.53    fast_tac} and the other tactics described below.
    1.54 @@ -555,16 +556,16 @@
    1.55  that sets up the classical reasoner.
    1.56  \begin{ttdescription}
    1.57  \item[\ttindexbold{fast_tac} $cs$ $i$] applies \texttt{step_tac} using
    1.58 -depth-first search, to prove subgoal~$i$.
    1.59 +depth-first search to prove subgoal~$i$.
    1.60  
    1.61  \item[\ttindexbold{best_tac} $cs$ $i$] applies \texttt{step_tac} using
    1.62 -best-first search, to prove subgoal~$i$.
    1.63 +best-first search to prove subgoal~$i$.
    1.64  
    1.65  \item[\ttindexbold{slow_tac} $cs$ $i$] applies \texttt{slow_step_tac} using
    1.66 -depth-first search, to prove subgoal~$i$.
    1.67 +depth-first search to prove subgoal~$i$.
    1.68  
    1.69 -\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} using
    1.70 -best-first search, to prove subgoal~$i$.
    1.71 +\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with
    1.72 +best-first search to prove subgoal~$i$.
    1.73  \end{ttdescription}
    1.74  
    1.75  
    1.76 @@ -613,8 +614,9 @@
    1.77  but allows unknowns to be instantiated.
    1.78  
    1.79  \item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
    1.80 -  procedure.  The (unsafe) wrapper tacticals are applied to a tactic that tries
    1.81 - \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule from~$cs$.
    1.82 +  procedure.  The unsafe wrapper tacticals are applied to a tactic that tries
    1.83 +  \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule
    1.84 +  from~$cs$.
    1.85  
    1.86  \item[\ttindexbold{slow_step_tac}] 
    1.87    resembles \texttt{step_tac}, but allows backtracking between using safe