# HG changeset patch
# User wenzelm
# Date 1136062178 -3600
# Node ID d995aecddc15d7b3f92149527a5eda6e03acc2f4
# Parent  540da24157515d9996da03a6fe19252c3a8b88ef
removed classical elim_format;

diff -r 540da2415751 -r d995aecddc15 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sat Dec 31 21:49:36 2005 +0100
+++ b/doc-src/IsarRef/generic.tex	Sat Dec 31 21:49:38 2005 +0100
@@ -1183,21 +1183,14 @@
 
 \subsubsection{Classical operations}
 
-\indexisaratt{elim-format}\indexisaratt{swapped}
+\indexisaratt{swapped}
 
 \begin{matharray}{rcl}
-  elim_format & : & \isaratt \\
   swapped & : & \isaratt \\
 \end{matharray}
 
 \begin{descr}
 
-\item [$elim_format$] turns a destruction rule into elimination rule format;
-  this operation is similar to the the intuitionistic version
-  (\S\ref{sec:misc-meth-att}), but each premise of the resulting rule acquires
-  an additional local fact of the negated main thesis; according to the
-  classical principle $(\neg A \Imp A) \Imp A$.
-
 \item [$swapped$] turns an introduction rule into an elimination, by resolving
   with the classical swap principle $(\neg B \Imp A) \Imp (\neg A \Imp B)$.