added infix delsimps
authornipkow
Fri Oct 29 11:54:50 1993 +0100 (1993-10-29)
changeset 889df4dfedee01
parent 87 c378e56d4a4b
child 89 2fee1120cb3e
added infix delsimps
src/Provers/simplifier.ML
     1.1 --- a/src/Provers/simplifier.ML	Fri Oct 29 11:53:43 1993 +0100
     1.2 +++ b/src/Provers/simplifier.ML	Fri Oct 29 11:54:50 1993 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Generic simplifier, suitable for most logics.
     1.5   
     1.6  *)
     1.7 -infix addsimps addeqcongs
     1.8 +infix addsimps addeqcongs delsimps
     1.9        setsolver setloop setmksimps setsubgoaler;
    1.10  
    1.11  signature SIMPLIFIER =
    1.12 @@ -14,6 +14,7 @@
    1.13    type simpset
    1.14    val addeqcongs: simpset * thm list -> simpset
    1.15    val addsimps: simpset * thm list -> simpset
    1.16 +  val delsimps: simpset * thm list -> simpset
    1.17    val asm_full_simp_tac: simpset -> int -> tactic
    1.18    val asm_simp_tac: simpset -> int -> tactic
    1.19    val empty_ss: simpset
    1.20 @@ -80,8 +81,7 @@
    1.21       loop_tac=loop_tac};
    1.22  
    1.23  fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews =
    1.24 -  let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews)
    1.25 -  in
    1.26 +  let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
    1.27    SS{mss= Thm.add_simps(mss,rews'),
    1.28       simps= rews' @ simps,
    1.29       congs= congs,
    1.30 @@ -90,6 +90,16 @@
    1.31       loop_tac=loop_tac}
    1.32    end;
    1.33  
    1.34 +fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews =
    1.35 +  let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
    1.36 +  SS{mss= Thm.del_simps(mss,rews'),
    1.37 +     simps= foldl (gen_rem eq_thm) (simps,rews'),
    1.38 +     congs= congs,
    1.39 +     subgoal_tac= subgoal_tac,
    1.40 +     finish_tac=finish_tac,
    1.41 +     loop_tac=loop_tac}
    1.42 +  end;
    1.43 +
    1.44  fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs newcongs =
    1.45    SS{mss= Thm.add_congs(mss,newcongs),
    1.46       simps= simps,