# HG changeset patch
# User wenzelm
# Date 1307304544 -7200
# Node ID ac4094f30a44676b01205bab04e288928ac14420
# Parent  41394a61cca9ebb4cdd2df56c3895eafe72a8058
removed somewhat low-level stuff (cf. attribute "swapped" in isar-ref);

diff -r 41394a61cca9 -r ac4094f30a44 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Sun Jun 05 22:02:54 2011 +0200
+++ b/doc-src/Ref/classical.tex	Sun Jun 05 22:09:04 2011 +0200
@@ -237,22 +237,6 @@
 resolution and also elim-resolution with the swapped form.
 \end{ttdescription}
 
-\subsection{Creating swapped rules}
-\begin{ttbox} 
-swapify   : thm list -> thm list
-joinrules : thm list * thm list -> (bool * thm) list
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the
-swapped versions of~{\it thms}, regarded as introduction rules.
-
-\item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]
-joins introduction rules, their swapped versions, and elimination rules for
-use with \ttindex{biresolve_tac}.  Each rule is paired with~\texttt{false}
-(indicating ordinary resolution) or~\texttt{true} (indicating
-elim-resolution).
-\end{ttdescription}
-
 
 \section{Setting up the classical reasoner}\label{sec:classical-setup}
 \index{classical reasoner!setting up}