# HG changeset patch
# User haftmann
# Date 1747851223 -7200
# Node ID 71f06e1f7fb4b3bff49472c4a28dc197b81ac1a2
# Parent  d374a7eb121abbda1cc198ff6b9702ff49a17a9a
provide list-valued interface for simp rules

diff -r d374a7eb121a -r 71f06e1f7fb4 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Wed May 21 20:13:43 2025 +0200
+++ b/src/Pure/raw_simplifier.ML	Wed May 21 20:13:43 2025 +0200
@@ -84,8 +84,11 @@
   val get_mksimps_context: Proof.context -> (thm -> Proof.context -> thm list * Proof.context)
   val set_mksimps_context: (thm -> Proof.context -> thm list * Proof.context) ->
     Proof.context -> Proof.context
+  val add_simps: thm list -> Proof.context -> Proof.context
   val add_simp: thm -> Proof.context -> Proof.context
+  val del_simps: thm list -> Proof.context -> Proof.context
   val del_simp: thm -> Proof.context -> Proof.context
+  val flip_simps: thm list -> Proof.context -> Proof.context
   val flip_simp: thm -> Proof.context -> Proof.context
   val mk_cong: Proof.context -> thm -> thm
   val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context
@@ -664,23 +667,27 @@
 *)
 in
 
-fun ctxt addsimps thms =
+fun add_simps thms ctxt =
   comb_simps insert_rrule (mk_rrule ctxt) false thms ctxt;
 
 fun add_flipped_simps thms ctxt =
   comb_simps insert_rrule (mk_rrule ctxt) true thms ctxt;
 
-fun ctxt delsimps thms =
+fun ctxt addsimps thms = ctxt |> add_simps thms;
+
+fun add_simp thm = add_simps [thm];
+
+fun del_simps thms ctxt =
   comb_simps (del_rrule true) (map mk_rrule2 o mk_rrule ctxt) false thms ctxt;
 
 fun del_simps_quiet thms ctxt =
   comb_simps (del_rrule false) (map mk_rrule2 o mk_rrule ctxt) false thms ctxt;
 
-fun add_simp thm ctxt = ctxt addsimps [thm];
+fun ctxt delsimps thms = ctxt |> del_simps thms;
 
-fun del_simp thm ctxt = ctxt delsimps [thm];
+fun del_simp thm = del_simps [thm];
 
-fun flip_simp thm = del_simps_quiet [thm] #> add_flipped_simps [thm];
+fun flip_simps thms = del_simps_quiet thms #> add_flipped_simps thms;
 (*
 with check for presence of symmetric version:
   if sym_present ctxt [thm]
@@ -688,6 +695,8 @@
   else ctxt addsimps [thm];
 *)
 
+fun flip_simp thm = flip_simps [thm];
+
 end;
 
 fun init_simpset thms ctxt = ctxt