doc-src/Ref/classical.tex

 where the order of the assumptions and the choice of~$Q@1$ are arbitrary.
 Elim-resolution plays a key role in simulating sequent proofs.
 
 We can easily handle reasoning on the left.
 As discussed in
-\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}}, 
+\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{{\S}\ref{destruct}}, 
 elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$
 achieves a similar effect as the corresponding sequent rules.  For the
 other connectives, we use sequent-style elimination rules instead of
 destruction rules such as $({\conj}E1,2)$ and $(\forall E)$.  But note that
 the rule $(\neg L)$ has no effect under our representation of sequents!

 Introduction rules are those that can be applied using ordinary resolution.
 The classical set automatically generates their swapped forms, which will
 be applied using elim-resolution.  Elimination rules are applied using
 elim-resolution.  In a classical set, rules are sorted by the number of new
 subgoals they will yield; rules that generate the fewest subgoals will be
-tried first (see \S\ref{biresolve_tac}).
+tried first (see {\S}\ref{biresolve_tac}).
 
 For elimination and destruction rules there are variants of the add operations
 adding a rule in a way such that it is applied only if also its second premise
 can be unified with an assumption of the current proof state:
 \indexbold{*addSE2}\indexbold{*addSD2}\indexbold{*addE2}\indexbold{*addD2}

 \label{sec:modifying-search}
 For a given classical set, the proof strategy is simple.  Perform as many safe
 inferences as possible; or else, apply certain safe rules, allowing
 instantiation of unknowns; or else, apply an unsafe rule.  The tactics also
 eliminate assumptions of the form $x=t$ by substitution if they have been set
-up to do so (see \texttt{hyp_subst_tacs} in~\S\ref{sec:classical-setup} below).
+up to do so (see \texttt{hyp_subst_tacs} in~{\S}\ref{sec:classical-setup} below).
 They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$
 and~$P$, then replace $P\imp Q$ by~$Q$.
 
 The classical reasoning tactics --- except \texttt{blast_tac}! --- allow
 you to modify this basic proof strategy by applying two lists of arbitrary 

 \begin{ttbox} 
 type wrapper = (int -> tactic) -> (int -> tactic);
 
 addSWrapper  : claset * (string *  wrapper       ) -> claset \hfill{\bf infix 4}
 addSbefore   : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
-addSaltern   : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
+addSafter    : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
 delSWrapper  : claset *  string                    -> claset \hfill{\bf infix 4}
 
 addWrapper   : claset * (string *  wrapper       ) -> claset \hfill{\bf infix 4}
 addbefore    : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
-addaltern    : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
+addafter     : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
 delWrapper   : claset *  string                    -> claset \hfill{\bf infix 4}
 
 addSss       : claset * simpset -> claset                 \hfill{\bf infix 4}
 addss        : claset * simpset -> claset                 \hfill{\bf infix 4}
 \end{ttbox}

 
 \item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore}
 adds the given tactic as a safe wrapper, such that it is tried 
 {\em before} each safe step of the search.
 
-\item[$cs$ addSaltern $(name,tac)$] \indexbold{*addSaltern}
+\item[$cs$ addSafter $(name,tac)$] \indexbold{*addSafter}
 adds the given tactic as a safe wrapper, such that it is tried 
 when a safe step of the search would fail.
 
 \item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper}
 deletes the safe wrapper with the given name.

 
 \item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore}
 adds the given tactic as an unsafe wrapper, such that it its result is 
 concatenated {\em before} the result of each unsafe step.
 
-\item[$cs$ addaltern $(name,tac)$] \indexbold{*addaltern}
+\item[$cs$ addafter $(name,tac)$] \indexbold{*addafter}
 adds the given tactic as an unsafe wrapper, such that it its result is 
 concatenated {\em after} the result of each unsafe step.
 
 \item[$cs$ delWrapper $name$] \indexbold{*delWrapper}
 deletes the unsafe wrapper with the given name.

 
 \index{simplification!from classical reasoner} 
 Strictly speaking, the operators \texttt{addss} and \texttt{addSss}
 are not part of the classical reasoner.
 , which are used as primitives 
-for the automatic tactics described in \S\ref{sec:automatic-tactics}, are
+for the automatic tactics described in {\S}\ref{sec:automatic-tactics}, are
 implemented as wrapper tacticals.
 they  
 \begin{warn}
 Being defined as wrappers, these operators are inappropriate for adding more 
 than one simpset at a time: the simpset added last overwrites any earlier ones.

 
 
 \section{The classical tactics}
 \index{classical reasoner!tactics} If installed, the classical module provides
 powerful theorem-proving tactics.  Most of them have capitalized analogues
-that use the default claset; see \S\ref{sec:current-claset}.
+that use the default claset; see {\S}\ref{sec:current-claset}.
 
 
 \subsection{The tableau prover}
 The tactic \texttt{blast_tac} searches for a proof using a fast tableau prover,
 coded directly in \ML.  It then reconstructs the proof using Isabelle

 completely. It tries to apply all fancy tactics it knows about, 
 performing a rather exhaustive search.
 \end{ttdescription}
 They must be supplied both a simpset and a claset; therefore 
 they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which 
-use the default claset and simpset (see \S\ref{sec:current-claset} below). 
+use the default claset and simpset (see {\S}\ref{sec:current-claset} below). 
 For interactive use, 
 the shorthand \texttt{auto();} abbreviates \texttt{by Auto_tac;} 
 while \texttt{force 1;} abbreviates \texttt{by (Force_tac 1);}
 
 

 \subsection{The current claset}\label{sec:current-claset}
 
 Each theory is equipped with an implicit \emph{current claset}
 \index{claset!current}.  This is a default set of classical
 rules.  The underlying idea is quite similar to that of a current
-simpset described in \S\ref{sec:simp-for-dummies}; please read that
+simpset described in {\S}\ref{sec:simp-for-dummies}; please read that
 section, including its warnings.  
 
 The tactics
 \begin{ttbox}
 Blast_tac        : int -> tactic