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