# HG changeset patch
# User oheimb
# Date 888574709 -3600
# Node ID ef6a546d6b69b0b5c38026b55f311d784e44cd02
# Parent  05d33fc7aa0811eaa27f3bd9331c0c47919fc9df
added minimal description of rep_cs

diff -r 05d33fc7aa08 -r ef6a546d6b69 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Fri Feb 27 11:18:16 1998 +0100
+++ b/doc-src/Ref/classical.tex	Fri Feb 27 11:18:29 1998 +0100
@@ -240,6 +240,12 @@
 \begin{ttbox} 
 empty_cs    : claset
 print_cs    : claset -> unit
+rep_cs      : claset -> {safeEs: thm list, safeIs: thm list,
+                         hazEs: thm list,  hazIs: thm list, 
+                         swrappers: (string * wrapper) list, 
+                         uwrappers: (string * wrapper) list,
+                         safe0_netpair: netpair, safep_netpair: netpair,
+                           haz_netpair: netpair,   dup_netpair: netpair}
 addSIs      : claset * thm list -> claset                 \hfill{\bf infix 4}
 addSEs      : claset * thm list -> claset                 \hfill{\bf infix 4}
 addSDs      : claset * thm list -> claset                 \hfill{\bf infix 4}
@@ -256,7 +262,14 @@
 \begin{ttdescription}
 \item[\ttindexbold{empty_cs}] is the empty classical set.
 
-\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.
+\item[\ttindexbold{print_cs} $cs$] displays the printable contents of~$cs$,
+  which is the rules. All other parts are non-printable.
+
+\item[\ttindexbold{rep_cs} $cs$] decomposes $cs$ as a record of its internal 
+  components, namely the safe intruduction and elimination rules, the unsafe
+  intruduction and elimination rules, the lists of safe and unsafe wrappers
+  (see \ref{sec:modifying-search}),
+  and the internal representation of the rules.
 
 \item[$cs$ addSIs $rules$] \indexbold{*addSIs}
 adds safe introduction~$rules$ to~$cs$.
@@ -302,6 +315,7 @@
 
 
 \subsection{Modifying the search step}
+\label{sec:modifying-search}
 For a given classical set, the proof strategy is simple.  Perform as many safe
 inferences as possible; or else, apply certain safe rules, allowing
 instantiation of unknowns; or else, apply an unsafe rule.  The tactics also