diff --git a/library/tools/tools.md b/library/tools/tools.md
index ea78c23f0..bc88f47d1 100644
--- a/library/tools/tools.md
+++ b/library/tools/tools.md
@@ -3,5 +3,4 @@ tools
 
 Various additional tools.
 
-* [tactic](tactic.lean) : reflected syntax for tactics
 * [helper_tactics](helper_tactics.lean) : useful tactics
\ No newline at end of file