doc-src/Ref/classical.tex

 \chapter{The Classical Reasoner}\label{chap:classical}
 \index{classical reasoner|(}
 \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
 
 Although Isabelle is generic, many users will be working in some
-extension of classical first-order logic.  Isabelle's set theory~{\tt
-  ZF} is built upon theory~\texttt{FOL}, while {\HOL}
-conceptually contains first-order logic as a fragment.
+extension of classical first-order logic.  
+Isabelle's set theory~{\tt ZF} is built upon theory~\texttt{FOL}, 
+while {\HOL} conceptually contains first-order logic as a fragment.
 Theorem-proving in predicate logic is undecidable, but many
 researchers have developed strategies to assist in this task.
 
 Isabelle's classical reasoner is an \ML{} functor that accepts certain
 information about a logic and delivers a suite of automatic tactics.  Each

   B$ is left as a conjunction.  Proof by assumption, Modus Ponens, etc., may be
   performed provided they do not instantiate unknowns.  Assumptions of the
   form $x=t$ may be eliminated.  The user-supplied safe wrapper tactical is
   applied.
 \item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but
-also does simplification with the given simpset. Still note that if the simpset 
-includes a splitter for the premises, the subgoal may be split.
+also does simplification with the given simpset. note that if the simpset 
+includes a splitter for the premises, the subgoal may still be split.
 \end{ttdescription}
 
 
 \subsection{Other classical tactics}
 \begin{ttbox} 

 
 \subsection{Accessing the current claset}
 \label{sec:access-current-claset}
 
 the functions to access the current claset are analogous to the functions 
-for the current simpset, so please see \label{sec:access-current-simpset}
+for the current simpset, so please see \ref{sec:access-current-simpset}
 for a description.
 \begin{ttbox}
 claset        : unit   -> claset
 claset_ref    : unit   -> claset ref
 claset_of     : theory -> claset
 claset_ref_of : theory -> claset ref
 print_claset  : theory -> unit
 CLASET        :(claset     ->       tactic) ->       tactic
 CLASET'       :(claset     -> 'a -> tactic) -> 'a -> tactic
-
 CLASIMPSET    :(clasimpset ->       tactic) ->       tactic
 CLASIMPSET'   :(clasimpset -> 'a -> tactic) -> 'a -> tactic
 \end{ttbox}