diff -r dc6ee60d2be8 -r ddaa1c133c5a doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Fri Sep 25 15:57:23 1998 +0200
+++ b/doc-src/Ref/classical.tex	Fri Sep 25 16:21:56 1998 +0200
@@ -4,9 +4,9 @@
 \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.
 
@@ -530,8 +530,8 @@
   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}
 
 
@@ -675,7 +675,7 @@
 \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
@@ -685,7 +685,6 @@
 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}