# HG changeset patch
# User wenzelm
# Date 1007517555 -3600
# Node ID f0fd3c4f2f492ced774c5929605bc2cc6b0aeb22
# Parent  a90156701dade7e1fbc00cf5901f20cc2b3f446a
removed AddXIs, AddXEs, AddXDs;

diff -r a90156701dad -r f0fd3c4f2f49 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Wed Dec 05 02:58:45 2001 +0100
+++ b/doc-src/Ref/classical.tex	Wed Dec 05 02:59:15 2001 +0100
@@ -671,17 +671,6 @@
 \end{ttbox}
 deletes rules from the current claset. 
 
-\medskip A few further functions are available as uppercase versions only:
-\begin{ttbox}
-AddXIs, AddXEs, AddXDs: thm list -> unit
-\end{ttbox}
-\indexbold{*AddXIs} \indexbold{*AddXEs} \indexbold{*AddXDs} augment the
-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
-not have any effect on classic Isabelle tactics.
-
 
 \subsection{Accessing the current claset}
 \label{sec:access-current-claset}