From 85a96579a55f1bb1a981019cbad3b26926021710 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Fri, 3 Feb 2023 16:31:56 +0100
Subject: [PATCH] remove tactic set for real

---
 server/testgame/TestGame/TacticDocs.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/server/testgame/TestGame/TacticDocs.lean b/server/testgame/TestGame/TacticDocs.lean
index fd33f0d..488aa67 100644
--- a/server/testgame/TestGame/TacticDocs.lean
+++ b/server/testgame/TestGame/TacticDocs.lean
@@ -258,5 +258,3 @@ Prove:
 
 TacticDoc intro
 "Useful to introduce stuff"
-
-TacticSet basics := rfl induction_on intro rewrite