doc-src/Ref/classical.tex
changeset 8702 78b7010db847
parent 8284 95c022a866ca
child 8926 0c7f90147f5d
equal deleted inserted replaced
8701:d1975e0c99af 8702:78b7010db847
   679 \end{ttbox}
   679 \end{ttbox}
   680 \indexbold{*AddXIs} \indexbold{*AddXEs} \indexbold{*AddXDs} augment the
   680 \indexbold{*AddXIs} \indexbold{*AddXEs} \indexbold{*AddXDs} augment the
   681 current claset by \emph{extra} introduction, elimination, or destruct rules.
   681 current claset by \emph{extra} introduction, elimination, or destruct rules.
   682 These provide additional hints for the basic non-automated proof methods of
   682 These provide additional hints for the basic non-automated proof methods of
   683 Isabelle/Isar \cite{isabelle-isar-ref}.  The corresponding Isar attributes are
   683 Isabelle/Isar \cite{isabelle-isar-ref}.  The corresponding Isar attributes are
   684 ``$intro!!$'', ``$elim!!$'', and ``$dest!!$''.  Note that these extra rules do
   684 ``$intro??$'', ``$elim??$'', and ``$dest??$''.  Note that these extra rules do
   685 not have any effect on classic Isabelle tactics.
   685 not have any effect on classic Isabelle tactics.
   686 
   686 
   687 
   687 
   688 \subsection{Accessing the current claset}
   688 \subsection{Accessing the current claset}
   689 \label{sec:access-current-claset}
   689 \label{sec:access-current-claset}