diff -r d1975e0c99af -r 78b7010db847 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Thu Apr 13 15:01:35 2000 +0200
+++ b/doc-src/Ref/classical.tex	Thu Apr 13 15:01:45 2000 +0200
@@ -681,7 +681,7 @@
 current claset by \emph{extra} introduction, elimination, or destruct rules.
 These provide additional hints for the basic non-automated proof methods of
 Isabelle/Isar \cite{isabelle-isar-ref}.  The corresponding Isar attributes are
-``$intro!!$'', ``$elim!!$'', and ``$dest!!$''.  Note that these extra rules do
+``$intro??$'', ``$elim??$'', and ``$dest??$''.  Note that these extra rules do
 not have any effect on classic Isabelle tactics.