--- a/doc-src/Ref/classical.tex Sun Jul 23 11:59:21 2000 +0200
+++ b/doc-src/Ref/classical.tex Sun Jul 23 12:01:05 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.