doc-src/Ref/classical.tex
changeset 9408 d3d56e1d2ec1
parent 8926 0c7f90147f5d
child 9439 a95343122ad0
     1.1 --- a/doc-src/Ref/classical.tex	Sun Jul 23 11:59:21 2000 +0200
     1.2 +++ b/doc-src/Ref/classical.tex	Sun Jul 23 12:01:05 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