diff -r f4599af94b83 -r 0c7f90147f5d doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Tue May 23 09:08:18 2000 +0200
+++ b/doc-src/Ref/classical.tex	Tue May 23 12:13:45 2000 +0200
@@ -257,7 +257,7 @@
 delrules : claset * thm list -> claset                 \hfill{\bf infix 4}
 \end{ttbox}
 The add operations ignore any rule already present in the claset with the same
-classification (such as Safe Introduction).  They print a warning if the rule
+classification (such as safe introduction).  They print a warning if the rule
 has already been added with some other classification, but add the rule
 anyway.  Calling \texttt{delrules} deletes all occurrences of a rule from the
 claset, but see the warning below concerning destruction rules.