From 37995edbd765b23673d8c849ea8279077eefc612 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 4 Jun 2015 17:58:39 -0400
Subject: [PATCH] fix(tools.md): remove missing link

---
 library/tools/tools.md | 1 -
 1 file changed, 1 deletion(-)

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