# HG changeset patch # User wenzelm # Date 964476770 -7200 # Node ID a95343122ad0c6d8825f28f3827fbb63eb3e6943 # Parent 6131037f8a1158c7d7f77cc1ee01a2f49d43c8f1 tuned; diff -r 6131037f8a11 -r a95343122ad0 doc-src/Ref/classical.tex --- 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}