# HG changeset patch
# User lcp
# Date 766420188 -7200
# Node ID f143f7686cd65260e326dff8a4425f6a49620f64
# Parent  a0e27395abe37bce815abbea571cf90e83860150
penultimate Springer draft

diff -r a0e27395abe3 -r f143f7686cd6 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Fri Apr 15 16:08:31 1994 +0200
+++ b/doc-src/Ref/classical.tex	Fri Apr 15 16:29:48 1994 +0200
@@ -1,5 +1,5 @@
 %% $Id$
-\chapter{The Classical Reasoner}
+\chapter{The Classical Reasoner}\label{chap:classical}
 \index{classical reasoner|(}
 \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
 
@@ -109,8 +109,9 @@
    \eqno({\neg}L) $$
 What about reasoning on the right?  Introduction rules can only affect the
 formula in the conclusion, namely~$Q@1$.  The other right-side formulae are
-represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.  In
-order to operate on one of these, it must first be exchanged with~$Q@1$.
+represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.  
+\index{assumptions!negated}
+In order to operate on one of these, it must first be exchanged with~$Q@1$.
 Elim-resolution with the {\bf swap} rule has this effect:
 $$ \List{\neg P; \; \neg R\Imp P} \Imp R   \eqno(swap)$$
 To ensure that swaps occur only when necessary, each introduction rule is
@@ -176,8 +177,8 @@
 
 
 \section{Classical rule sets}
-\index{classical sets|bold}
-Each automatic tactic takes a {\bf classical rule set} --- a collection of
+\index{classical sets}
+Each automatic tactic takes a {\bf classical set} --- a collection of
 rules, classified as introduction or elimination and as {\bf safe} or {\bf
 unsafe}.  In general, safe rules can be attempted blindly, while unsafe
 rules must be used with care.  A safe rule must never reduce a provable
@@ -203,7 +204,7 @@
 is unsafe if it instantiates unknowns shared with other subgoals --- thus
 \ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.
 
-Classical rule sets belong to the abstract type \ttindexbold{claset}, which
+Classical rule sets belong to the abstract type \mltydx{claset}, which
 supports the following operations (provided the classical reasoner is
 installed!):
 \begin{ttbox} 
@@ -252,14 +253,13 @@
 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 may
-also apply \ttindex{hyp_subst_tac}, if they have been set up to do so (see
+also apply {\tt hyp_subst_tac}, if they have been set up to do so (see
 below).  They may perform a form of Modus Ponens: if there are assumptions
 $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$.
 
 
 \section{The classical tactics}
-\index{classical prover!tactics|bold}
-\index{tactics!for classical proof|bold}
+\index{classical reasoner!tactics}
 If installed, the classical module provides several tactics (and other
 operations) for simulating the classical sequent calculus.
 
@@ -275,8 +275,8 @@
 yourself, you can execute these procedures one step at a time.
 \begin{ttdescription}
 \item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
-subgoal~$i$.  This may include proof by assumption or Modus Ponens, taking
-care not to instantiate unknowns, or \ttindex{hyp_subst_tac}.
+subgoal~$i$.  This may include proof by assumption or Modus Ponens (taking
+care not to instantiate unknowns), or {\tt hyp_subst_tac}.
 
 \item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all 
 subgoals.  It is deterministic, with at most one outcome.  If the automatic
@@ -319,8 +319,8 @@
 
 
 \subsection{Other useful tactics}
-\index{tactics!for contradiction|bold}
-\index{tactics!for Modus Ponens|bold}
+\index{tactics!for contradiction}
+\index{tactics!for Modus Ponens}
 \begin{ttbox} 
 contr_tac    :             int -> tactic
 mp_tac       :             int -> tactic
@@ -329,10 +329,11 @@
 \end{ttbox}
 These can be used in the body of a specialized search.
 \begin{ttdescription}
-\item[\ttindexbold{contr_tac} {\it i}] solves subgoal~$i$ by detecting a
-contradiction among two assumptions of the form $P$ and~$\neg P$, or fail.
-It may instantiate unknowns.  The tactic can produce multiple outcomes,
-enumerating all possible contradictions.
+\item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}
+  solves subgoal~$i$ by detecting a contradiction among two assumptions of
+  the form $P$ and~$\neg P$, or fail.  It may instantiate unknowns.  The
+  tactic can produce multiple outcomes, enumerating all possible
+  contradictions.
 
 \item[\ttindexbold{mp_tac} {\it i}] 
 is like {\tt contr_tac}, but also attempts to perform Modus Ponens in
@@ -346,7 +347,7 @@
 
 \item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
 the proof state using {\it thms}, which should be a list of introduction
-rules.  First, it attempts to solve the goal using \ttindex{assume_tac} or
+rules.  First, it attempts to solve the goal using {\tt assume_tac} or
 {\tt contr_tac}.  It then attempts to apply each rule in turn, attempting
 resolution and also elim-resolution with the swapped form.
 \end{ttdescription}
@@ -369,12 +370,12 @@
 
 
 \section{Setting up the classical reasoner}
-\index{classical reasoner!setting up|bold}
+\index{classical reasoner!setting up}
 Isabelle's classical object-logics, including {\tt FOL} and {\tt HOL}, have
 the classical reasoner already set up.  When defining a new classical logic,
 you should set up the reasoner yourself.  It consists of the \ML{} functor
 \ttindex{ClassicalFun}, which takes the argument
-signature\indexbold{*CLASSICAL_DATA}
+signature {\tt CLASSICAL_DATA}:
 \begin{ttbox} 
 signature CLASSICAL_DATA =
   sig
@@ -387,13 +388,13 @@
 \end{ttbox}
 Thus, the functor requires the following items:
 \begin{ttdescription}
-\item[\ttindexbold{mp}] should be the Modus Ponens rule
+\item[\tdxbold{mp}] should be the Modus Ponens rule
 $\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
 
-\item[\ttindexbold{not_elim}] should be the contradiction rule
+\item[\tdxbold{not_elim}] should be the contradiction rule
 $\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.
 
-\item[\ttindexbold{swap}] should be the swap rule
+\item[\tdxbold{swap}] should be the swap rule
 $\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.
 
 \item[\ttindexbold{sizef}] is the heuristic function used for best-first
@@ -403,7 +404,7 @@
 those concerned with type checking).  A heuristic function might simply
 count the subgoals.
 
-\item[\ttindexbold{hyp_subst_tac}] is a list of tactics for substitution in
+\item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
 the hypotheses, typically created by \ttindex{HypsubstFun} (see
 Chapter~\ref{substitution}).  This list can, of course, be empty.  The
 tactics are assumed to be safe!
@@ -411,6 +412,6 @@
 The functor is not at all sensitive to the formalization of the
 object-logic.  It does not even examine the rules, but merely applies them
 according to its fixed strategy.  The functor resides in {\tt
-Provers/classical.ML} on the Isabelle distribution directory.
+Provers/classical.ML} in the Isabelle distribution directory.
 
-\index{classical prover|)}
+\index{classical reasoner|)}