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