# HG changeset patch
# User oheimb
# Date 888417932 -3600
# Node ID 89ad3eb863a15b72f4ed2506e3ae211088824829
# Parent  f04da668581cd5758581e9968641a806fb89e035
changed wrapper mechanism of classical reasoner

diff -r f04da668581c -r 89ad3eb863a1 NEWS
--- a/NEWS	Tue Feb 24 11:35:33 1998 +0100
+++ b/NEWS	Wed Feb 25 15:45:32 1998 +0100
@@ -1,7 +1,23 @@
+
+
 
 Isabelle NEWS -- history of user-visible changes
 ================================================
 
+New in Isabelle98? (???)
+-----------------------
+
+* changed wrapper mechanism for the classical reasoner now allows for selected
+  deletion of wrappers, by introduction of names for wrapper functionals.
+  This implies that addbefore, addSbefore, addaltern, and addSaltern now take
+  a pair (name, tactic) as argument, and that adding two tactics with the same
+  name overwrites the first one (emitting a warning).
+  setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by
+  addWrapper, addSWrapper: claset * wrapper -> claset
+  delWrapper, delSWrapper: claset *  string -> claset
+  getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
+
+
 New in Isabelle98 (January 1998)
 --------------------------------
 
diff -r f04da668581c -r 89ad3eb863a1 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Tue Feb 24 11:35:33 1998 +0100
+++ b/doc-src/Ref/classical.tex	Wed Feb 25 15:45:32 1998 +0100
@@ -311,29 +311,33 @@
 and~$P$, then replace $P\imp Q$ by~$Q$.
 
 The classical reasoning tactics --- except \texttt{blast_tac}! --- allow
-you to modify this basic proof strategy by 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{step_tac}, \ttindex{slow_step_tac} and the tactics that call
-them.
+you to modify this basic proof strategy by applying two lists of arbitrary 
+{\bf wrapper tacticals} to it. 
+The first wrapper list, which is considered to contain safe wrappers only, 
+affects \ttindex{safe_step_tac} and all the tactics that call it.  
+The second one, which may contain unsafe wrappers, affects \ttindex{step_tac}, 
+\ttindex{slow_step_tac} and the tactics that call them.
+A wrapper transforms each step of the search, for example 
+by invoking other tactics before or alternatively to the original step tactic. 
+All members of a wrapper list are applied in turn to the respective step tactic.
+
+Initially the two wrapper lists are empty, which means no modification of the
+step tactics. Safe and unsafe wrappers are added to a claset 
+with the functions given below, supplying them with wrapper names. 
+These names may be used to selectively delete wrappers.
 
 \begin{ttbox} 
+type wrapper = (int -> tactic) -> (int -> tactic);
+addSbefore   : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
+addSaltern   : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
+addSWrapper  : claset * (string * wrapper        ) -> claset \hfill{\bf infix 4}
+delSWrapper  : claset *  string                    -> claset \hfill{\bf infix 4}
+addbefore    : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
+addaltern    : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
+addWrapper   : claset * (string * wrapper        ) -> claset \hfill{\bf infix 4}
+delWrapper   : claset *  string                    -> 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} The wrapper tacticals
@@ -343,7 +347,7 @@
 installed:
 \begin{ttbox}
 infix 4 addss;
-fun cs addss  ss = cs  addbefore  asm_full_simp_tac ss;
+fun cs addss ss = cs addbefore asm_full_simp_tac ss;
 \end{ttbox}
 
 \begin{ttdescription}
diff -r f04da668581c -r 89ad3eb863a1 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Tue Feb 24 11:35:33 1998 +0100
+++ b/src/FOL/simpdata.ML	Wed Feb 25 15:45:32 1998 +0100
@@ -334,8 +334,9 @@
 
 (*Add a simpset to a classical set!*)
 infix 4 addSss addss;
-fun cs addSss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
-fun cs addss  ss = cs addbefore                        asm_full_simp_tac ss;
+fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac",
+				  CHANGED o (safe_asm_more_full_simp_tac ss));
+fun cs addss  ss = cs addbefore  ("asm_full_simp_tac", asm_full_simp_tac ss);
 
 fun Addss ss = (claset_ref() := claset() addss ss);