--- 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}
--- 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