--- 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)$.