# HG changeset patch
# User oheimb
# Date 856024553 -3600
# Node ID 1612b99395d41e19785a2d81e8558171864ffa1a
# Parent  5e5c78ba955e80cf14ce307c6e8d708bc4f60be6
corrected minor mistakes

diff -r 5e5c78ba955e -r 1612b99395d4 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Sat Feb 15 17:02:19 1997 +0100
+++ b/doc-src/Ref/classical.tex	Sat Feb 15 17:35:53 1997 +0100
@@ -273,23 +273,27 @@
 $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$.
 
 The classical reasoner allows you to modify this basic proof strategy by
-applying two arbitrary {\bf wrapper tactical}s to it. This affects each step of
+applying two arbitrary {\bf wrapper tacticals} to it. This affects each step of
 the search.  Usually they are the identity tacticals, but they could apply 
 another tactic before or after the step tactic. The first one, which is
 considered to be safe, affects \ttindex{safe_step_tac} and all the tactics that
 call it. The the second one, which may be unsafe, affects 
-\ttindex{safe_step_tac}, \ttindex{slow_step_tac} and the tactics that call them.
+\ttindex{step_tac}, \ttindex{slow_step_tac} and the tactics that call them.
 
 \begin{ttbox} 
-addss       : claset * simpset -> claset                  \hfill{\bf infix 4}
-addSbefore   : claset * (int -> tactic) -> claset         \hfill{\bf infix 4}
-addSaltern   : claset * (int -> tactic) -> claset         \hfill{\bf infix 4}
-setSWrapper  : claset * ((int -> tactic) -> (int -> tactic)) -> claset \hfill{\bf infix 4}
-compSWrapper : claset * ((int -> tactic) -> (int -> tactic)) -> claset \hfill{\bf infix 4}
-addbefore    : claset * (int -> tactic) -> claset         \hfill{\bf infix 4}
-addaltern    : claset * (int -> tactic) -> claset         \hfill{\bf infix 4}
-setWrapper   : claset * ((int -> tactic) -> (int -> tactic)) -> claset \hfill{\bf infix 4}
-compWrapper  : claset * ((int -> tactic) -> (int -> tactic)) -> claset \hfill{\bf infix 4}
+addss        : claset * simpset -> claset                 \hfill{\bf infix 4}
+addSbefore   : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}
+addSaltern   : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}
+setSWrapper  : claset * ((int -> tactic) -> 
+                         (int -> tactic)) -> claset       \hfill{\bf infix 4}
+compSWrapper : claset * ((int -> tactic) -> 
+                         (int -> tactic)) -> claset       \hfill{\bf infix 4}
+addbefore    : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}
+addaltern    : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}
+setWrapper   : claset * ((int -> tactic) -> 
+                         (int -> tactic)) -> claset       \hfill{\bf infix 4}
+compWrapper  : claset * ((int -> tactic) -> 
+                         (int -> tactic)) -> claset       \hfill{\bf infix 4}
 \end{ttbox}
 %
 \index{simplification!from classical reasoner} 
diff -r 5e5c78ba955e -r 1612b99395d4 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Sat Feb 15 17:02:19 1997 +0100
+++ b/doc-src/Ref/simplifier.tex	Sat Feb 15 17:35:53 1997 +0100
@@ -278,8 +278,8 @@
 rewrite rule whose condition contains extra variables. When a simplification 
 tactic is to be combined with other provers, especially with the classical 
 reasoner, it is important whether it can be considered safe or not. Therefore,
-solver is split into a safe and anunsafe part. Both parts of the solver,
-which are stored within the simpset, can be set independently using 
+the solver is split into a safe and anunsafe part. Both parts can be set 
+independently of each other using 
 \ttindex{setSSolver} (with a safe tactic as argument) and \ttindex{setSolver}
 (with an unsafe tactic) . Additional solvers, which are tried after the already
 set solvers, may be added using \ttindex{addSSolver} and \ttindex{addSolver}. 
@@ -369,11 +369,6 @@
 
 signature SIMPLIFIER =
 sig
-  type simproc
-  val mk_simproc: string -> cterm list -> (Sign.sg -> term -> thm option) -> simproc
-  val name_of_simproc: simproc -> string
-  val conv_prover: (term * term -> term) -> thm -> (thm -> thm)
-    -> tactic -> (int -> tactic) -> Sign.sg -> term -> term -> thm      (* FIXME move?, rename? *)
   type simpset
   val empty_ss: simpset
   val rep_ss: simpset -> {simps: thm list, procs: string list, congs: thm list,
@@ -977,9 +972,9 @@
 \index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler}
 \index{*addsimps}\index{*addcongs}
 \begin{ttbox}
-fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
+fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls \at prems),
                                  atac, etac FalseE];
-fun   safe_solver prems = FIRST'[match_tac (triv_rls@prems),
+fun   safe_solver prems = FIRST'[match_tac (triv_rls \at prems),
                                  eq_assume_tac, ematch_tac [FalseE]];
 val IFOL_ss = empty_ss setsubgoaler asm_simp_tac
                        setSSolver   safe_solver