diff --git a/src/Lean/Elab/Tactic/BoolToPropSimps.lean b/src/Lean/Elab/Tactic/BoolToPropSimps.lean
index 681680461c16..e14ce2fc3d41 100644
--- a/src/Lean/Elab/Tactic/BoolToPropSimps.lean
+++ b/src/Lean/Elab/Tactic/BoolToPropSimps.lean
@@ -7,6 +7,11 @@ Authors: Tobias Grosser
 prelude
 import Lean.Meta.Tactic.Simp.Attr
 
+builtin_initialize bool_to_prop : Lean.Meta.SimpExtension ←
+  Lean.Meta.registerSimpAttr `bool_to_prop
+    "simp lemmas converting boolean expressions in terms of `decide` into propositional statements"
+
+@[deprecated bool_to_prop (since := "2025-02-10")]
 builtin_initialize boolToPropSimps : Lean.Meta.SimpExtension ←
   Lean.Meta.registerSimpAttr `boolToPropSimps
     "simp lemmas converting boolean expressions in terms of `decide` into propositional statements"
diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean
index e985a8b9ada7..ce08b338ab79 100644
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean
@@ -689,6 +689,11 @@ def evalOmega : Tactic
     omegaTactic cfg
   | _ => throwUnsupportedSyntax
 
+builtin_initialize bitvec_to_nat : SimpExtension ←
+  registerSimpAttr `bitvec_to_nat
+    "simp lemmas converting `BitVec` goals to `Nat` goals"
+
+@[deprecated bitvec_to_nat (since := "2025-02-10")]
 builtin_initialize bvOmegaSimpExtension : SimpExtension ←
   registerSimpAttr `bv_toNat
     "simp lemmas converting `BitVec` goals to `Nat` goals, for the `bv_omega` preprocessor"