diff --git a/ProofWidgets/Component/HtmlDisplay.lean b/ProofWidgets/Component/HtmlDisplay.lean
index 85e8eee..e59c655 100644
--- a/ProofWidgets/Component/HtmlDisplay.lean
+++ b/ProofWidgets/Component/HtmlDisplay.lean
@@ -71,18 +71,6 @@ def elabHtmlCmd : CommandElab := fun
       stx
   | stx => throwError "Unexpected syntax {stx}."
 
-/-- The `html!` tactic is deprecated and does nothing.
-If you have a use for it,
-please open an issue on https://github.com/leanprover-community/ProofWidgets4. -/
-@[deprecated "The `html!` tactic is deprecated and does nothing. If you have a use for it, \
-  please open an issue on https://github.com/leanprover-community/ProofWidgets4."
-  (since := "2024-05-15")]
-syntax (name := htmlTac) "html! " term : tactic
-
-open Tactic in
-@[tactic htmlTac]
-def elabHtmlTac : Tactic | _ => pure ()
-
 end HtmlCommand
 end ProofWidgets