# HG changeset patch
# User nipkow
# Date 751892090 -3600
# Node ID 9df4dfedee01eb1aec3be583e256211708c9c5ad
# Parent  c378e56d4a4b461078742af79935c5c4b265e730
added infix delsimps

diff -r c378e56d4a4b -r 9df4dfedee01 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Fri Oct 29 11:53:43 1993 +0100
+++ b/src/Provers/simplifier.ML	Fri Oct 29 11:54:50 1993 +0100
@@ -6,7 +6,7 @@
 Generic simplifier, suitable for most logics.
  
 *)
-infix addsimps addeqcongs
+infix addsimps addeqcongs delsimps
       setsolver setloop setmksimps setsubgoaler;
 
 signature SIMPLIFIER =
@@ -14,6 +14,7 @@
   type simpset
   val addeqcongs: simpset * thm list -> simpset
   val addsimps: simpset * thm list -> simpset
+  val delsimps: simpset * thm list -> simpset
   val asm_full_simp_tac: simpset -> int -> tactic
   val asm_simp_tac: simpset -> int -> tactic
   val empty_ss: simpset
@@ -80,8 +81,7 @@
      loop_tac=loop_tac};
 
 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews =
-  let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews)
-  in
+  let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
   SS{mss= Thm.add_simps(mss,rews'),
      simps= rews' @ simps,
      congs= congs,
@@ -90,6 +90,16 @@
      loop_tac=loop_tac}
   end;
 
+fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews =
+  let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
+  SS{mss= Thm.del_simps(mss,rews'),
+     simps= foldl (gen_rem eq_thm) (simps,rews'),
+     congs= congs,
+     subgoal_tac= subgoal_tac,
+     finish_tac=finish_tac,
+     loop_tac=loop_tac}
+  end;
+
 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs newcongs =
   SS{mss= Thm.add_congs(mss,newcongs),
      simps= simps,