1.1 --- a/doc-src/Ref/classical.tex Mon Jan 12 17:48:55 1998 +0100
1.2 +++ b/doc-src/Ref/classical.tex Mon Jan 12 17:49:12 1998 +0100
1.3 @@ -558,12 +558,22 @@
1.4 \end{ttdescription}
1.5
1.6 \subsection{The current claset}\label{sec:current-claset}
1.7 -Some logics (\FOL, {\HOL} and \ZF) support the concept of a current
1.8 -claset\index{claset!current}. This is a default set of classical rules. The
1.9 -underlying idea is quite similar to that of a current simpset described in
1.10 -\S\ref{sec:simp-for-dummies}; please read that section, including its
1.11 -warnings. Just like simpsets, clasets can be associated with theories. The
1.12 -tactics
1.13 +
1.14 +Each theory is equipped with an implicit \emph{current
1.15 + claset}\index{claset!current}. This is a default set of classical
1.16 +rules. The underlying idea is quite similar to that of a current
1.17 +simpset described in \S\ref{sec:simp-for-dummies}; please read that
1.18 +section, including its warnings. The implicit claset can be accessed
1.19 +as follows:
1.20 +\begin{ttbox}
1.21 +claset : unit -> claset
1.22 +claset_ref : unit -> claset ref
1.23 +claset_of : theory -> claset
1.24 +claset_ref_of : theory -> claset ref
1.25 +print_claset : theory -> unit
1.26 +\end{ttbox}
1.27 +
1.28 +The tactics
1.29 \begin{ttbox}
1.30 Blast_tac : int -> tactic
1.31 Auto_tac : tactic
1.32 @@ -584,10 +594,10 @@
1.33 \indexbold{*Step_tac}
1.34 make use of the current claset. For example, \texttt{Blast_tac} is defined as
1.35 \begin{ttbox}
1.36 -fun Blast_tac i st = blast_tac (!claset) i st;
1.37 +fun Blast_tac i st = blast_tac (claset()) i st;
1.38 \end{ttbox}
1.39 -and gets the current claset, \ttindex{!claset}, only after it is applied to a
1.40 -proof state. The functions
1.41 +and gets the current claset, only after it is applied to a proof
1.42 +state. The functions
1.43 \begin{ttbox}
1.44 AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit
1.45 \end{ttbox}
2.1 --- a/doc-src/Ref/ref.ind Mon Jan 12 17:48:55 1998 +0100
2.2 +++ b/doc-src/Ref/ref.ind Mon Jan 12 17:49:12 1998 +0100
2.3 @@ -4,8 +4,6 @@
2.4 \subitem in main goal, 8
2.5 \item {\tt\$}, \bold{60}, 86
2.6 \item {\tt\%} symbol, 69
2.7 - \item *
2.8 - \subitem claset, 137
2.9 \item {\tt ::} symbol, 69, 70
2.10 \item {\tt ==} symbol, 69
2.11 \item {\tt ==>} symbol, 69