changeset 8926 0c7f90147f5d
parent 8702 78b7010db847
child 9408 d3d56e1d2ec1
--- 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}
 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.