# HG changeset patch
# User nipkow
# Date 889194029 -3600
# Node ID ff081854fc863e3fe0370db074ade13fbc7232c7
# Parent  a331c1f5a23e51d7ff887ae907cfc31ebc08f721
Added delspilts, Addsplits, Delsplits.

diff -r a331c1f5a23e -r ff081854fc86 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Fri Mar 06 15:19:29 1998 +0100
+++ b/src/Provers/simplifier.ML	Fri Mar 06 15:20:29 1998 +0100
@@ -7,7 +7,7 @@
 *)
 
 infix 4
-  setsubgoaler setloop addloop setSSolver addSSolver setSolver
+  setsubgoaler setloop addloop delloop setSSolver addSSolver setSolver
   addSolver addsimps delsimps addeqcongs deleqcongs
   setmksimps setmkeqTrue setmksym settermless addsimprocs delsimprocs;
 
@@ -30,6 +30,7 @@
   val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
   val setloop:      simpset *             (int -> tactic) -> simpset
   val addloop:      simpset *  (string * (int -> tactic)) -> simpset
+  val delloop:      simpset *   string                    -> simpset
   val setSSolver:   simpset * (thm list -> int -> tactic) -> simpset
   val addSSolver:   simpset * (thm list -> int -> tactic) -> simpset
   val setSolver:    simpset * (thm list -> int -> tactic) -> simpset
@@ -152,6 +153,13 @@
   make_ss (mss, subgoal_tac, overwrite(loop_tacs,atac),
            finish_tac, unsafe_finish_tac);
 
+fun (ss as Simpset {mss,subgoal_tac,loop_tacs,finish_tac,unsafe_finish_tac})
+    delloop name =
+  let val (del,rest) = partition (fn (n,_) => n=name) loop_tacs
+  in if null del then (warning ("No such looper in simpset: " ^ name); ss)
+     else make_ss (mss, subgoal_tac, rest, finish_tac, unsafe_finish_tac)
+  end;
+
 fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac = _, unsafe_finish_tac})
     setSSolver finish_tac =
   make_ss (mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);