tuned;
authorwenzelm
Tue, 25 Jul 2000 00:12:50 +0200
changeset 9439a95343122ad0
parent 9438 6131037f8a11
child 9440 a72fe5eafb5e
tuned;
doc-src/Ref/classical.tex
     1.1 --- a/doc-src/Ref/classical.tex	Tue Jul 25 00:12:39 2000 +0200
     1.2 +++ b/doc-src/Ref/classical.tex	Tue Jul 25 00:12:50 2000 +0200
     1.3 @@ -532,7 +532,7 @@
     1.4    form $x=t$ may be eliminated.  The user-supplied safe wrapper tactical is
     1.5    applied.
     1.6  \item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but
     1.7 -also does simplification with the given simpset. note that if the simpset 
     1.8 +also does simplification with the given simpset. Note that if the simpset 
     1.9  includes a splitter for the premises, the subgoal may still be split.
    1.10  \end{ttdescription}
    1.11