src/Pure/simplifier.ML

--- a/src/Pure/simplifier.ML	Wed Aug 14 13:51:36 2024 +0200
+++ b/src/Pure/simplifier.ML	Wed Aug 14 15:30:29 2024 +0200
@@ -28,6 +28,8 @@
 signature SIMPLIFIER =
 sig
   include BASIC_SIMPLIFIER
+  val dest_simps: simpset -> (Thm_Name.T * thm) list
+  val dest_congs: simpset -> (cong_name * thm) list
   val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
   val attrib: (thm -> Proof.context -> Proof.context) -> attribute
   val simp_add: attribute