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