doc-src/Ref/classical.tex
changeset 7990 0a604b2fc2b1
parent 6592 c120262044b6
child 8136 8c65f3ca13f2
     1.1 --- a/doc-src/Ref/classical.tex	Sun Oct 31 15:26:37 1999 +0100
     1.2 +++ b/doc-src/Ref/classical.tex	Sun Oct 31 20:11:23 1999 +0100
     1.3 @@ -670,6 +670,17 @@
     1.4  \end{ttbox}
     1.5  deletes rules from the current claset. 
     1.6  
     1.7 +\medskip A few further functions are available as uppercase versions only:
     1.8 +\begin{ttbox}
     1.9 +AddXIs, AddXEs, AddXDs: thm list -> unit
    1.10 +\end{ttbox}
    1.11 +\indexbold{*AddXIs} \indexbold{*AddXEs} \indexbold{*AddXDs} augment the
    1.12 +current claset by \emph{extra} introduction, elimination, or destruct rules.
    1.13 +These provide additional hints for the basic non-automated proof methods of
    1.14 +Isabelle/Isar \cite{isabelle-isar-ref}.  The corresponding Isar attributes are
    1.15 +``$intro!!$'', ``$elim!!$'', and ``$dest!!$''.  Note that these extra rules do
    1.16 +not have any effect on classic Isabelle tactics.
    1.17 +
    1.18  
    1.19  \subsection{Accessing the current claset}
    1.20  \label{sec:access-current-claset}