doc-src/Ref/classical.tex
changeset 9439 a95343122ad0
parent 9408 d3d56e1d2ec1
child 9695 ec7d7f877712
--- a/doc-src/Ref/classical.tex	Tue Jul 25 00:12:39 2000 +0200
+++ b/doc-src/Ref/classical.tex	Tue Jul 25 00:12:50 2000 +0200
@@ -532,7 +532,7 @@
   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. note that if the simpset 
+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}