remove tactic set for real

3 years ago · 85a96579a5
parent d1eee327dd
commit 85a96579a5
1 changed files with 0 additions and 2 deletions
--- 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