1.1 --- a/doc-src/Ref/classical.tex	Fri Feb 27 11:18:16 1998 +0100
     1.2 +++ b/doc-src/Ref/classical.tex	Fri Feb 27 11:18:29 1998 +0100
     1.3 @@ -240,6 +240,12 @@
     1.4  \begin{ttbox} 
     1.5  empty_cs    : claset
     1.6  print_cs    : claset -> unit
     1.7 +rep_cs      : claset -> {safeEs: thm list, safeIs: thm list,
     1.8 +                         hazEs: thm list,  hazIs: thm list, 
     1.9 +                         swrappers: (string * wrapper) list, 
    1.10 +                         uwrappers: (string * wrapper) list,
    1.11 +                         safe0_netpair: netpair, safep_netpair: netpair,
    1.12 +                           haz_netpair: netpair,   dup_netpair: netpair}
    1.13  addSIs      : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.14  addSEs      : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.15  addSDs      : claset * thm list -> claset                 \hfill{\bf infix 4}
    1.16 @@ -256,7 +262,14 @@
    1.17  \begin{ttdescription}
    1.18  \item[\ttindexbold{empty_cs}] is the empty classical set.
    1.19  
    1.20 -\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.
    1.21 +\item[\ttindexbold{print_cs} $cs$] displays the printable contents of~$cs$,
    1.22 +  which is the rules. All other parts are non-printable.
    1.23 +
    1.24 +\item[\ttindexbold{rep_cs} $cs$] decomposes $cs$ as a record of its internal 
    1.25 +  components, namely the safe intruduction and elimination rules, the unsafe
    1.26 +  intruduction and elimination rules, the lists of safe and unsafe wrappers
    1.27 +  (see \ref{sec:modifying-search}),
    1.28 +  and the internal representation of the rules.
    1.29  
    1.30  \item[$cs$ addSIs $rules$] \indexbold{*addSIs}
    1.31  adds safe introduction~$rules$ to~$cs$.
    1.32 @@ -302,6 +315,7 @@
    1.33  
    1.34  
    1.35  \subsection{Modifying the search step}
    1.36 +\label{sec:modifying-search}
    1.37  For a given classical set, the proof strategy is simple.  Perform as many safe
    1.38  inferences as possible; or else, apply certain safe rules, allowing
    1.39  instantiation of unknowns; or else, apply an unsafe rule.  The tactics also