diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index f211b1c..38bae1e 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -193,6 +193,9 @@ entry or a tactic doc set. -/
 elab "NewTactics" args:ident* : command => do
   modifyCurLevel fun level => pure {level with newTactics := args.map (·.getId)}
 
+elab "DisabledTactics" args:ident* : command => do
+  modifyCurLevel fun level => pure {level with disabledTactics := args.map (·.getId)}
+
 /-! ## Lemmas -/
 
 /-- Declare a documentation entry for some lemma.
diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean
index a9f989b..b0dc577 100644
--- a/server/leanserver/GameServer/FileWorker.lean
+++ b/server/leanserver/GameServer/FileWorker.lean
@@ -64,19 +64,33 @@ open JsonRpc
 
 section Elab
 
--- TODO: use HashSetf ro `allowed`?
+-- TODO: use HashSet for allowed tactics?
 /-- Find all tactics in syntax object that are forbidden according to a
 set `allowed` of allowed tactics. -/
-partial def findForbiddenTactics (allowed: Array Name) (stx : Syntax)
-    (acc : Array (SourceInfo × String) := #[]) : Array (SourceInfo × String) :=
+partial def findForbiddenTactics (inputCtx : Parser.InputContext) (level : GameLevel) (stx : Syntax)
+  : Elab.Command.CommandElabM Unit := do
   match stx with
-  | .missing => acc
-  | .node info kind args => args.foldl (fun acc s => findForbiddenTactics allowed s acc) acc
-  | .atom info val => if isForbidden val then acc.push (info, val) else acc
-  | .ident info rawVal val preresolved => acc
-where isForbidden (val : String) : Bool :=
-  0 < val.length ∧ val.data[0]!.isAlpha ∧ ¬ allowed.contains val
-
+  | .missing => return ()
+  | .node info kind args =>
+    for arg in args do
+      findForbiddenTactics inputCtx level arg
+  | .atom info val =>
+    -- ignore syntax elements that do not start with a letter
+    if 0 < val.length ∧ val.data[0]!.isAlpha then
+      if ¬ ((level.tactics.map (·.name.toString))).contains val then
+        addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!"
+      else if level.disabledTactics.contains val then
+        addErrorMessage info s!"The tactic '{val}' is disabled in this level!"
+  | .ident info rawVal val preresolved => return ()
+where addErrorMessage (info : SourceInfo) (s : MessageData) :=
+  modify fun st => { st with
+    messages := st.messages.add {
+      fileName := inputCtx.fileName
+      severity := MessageSeverity.error
+      pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
+      data     := s
+    }
+  }
 
 open Elab Meta Expr in
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool) (couldBeEndSnap : Bool) : IO Snapshot := do
@@ -114,16 +128,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           let level ← GameServer.getLevelByFileName inputCtx.fileName
 
           -- Check for forbidden tactics
-          let forbiddenTacs := findForbiddenTactics (level.tactics.map (·.name)) tacticStx
-          for (info, forbiddenTac) in forbiddenTacs do
-            modify fun st => { st with
-              messages := st.messages.add {
-                fileName := inputCtx.fileName
-                severity := MessageSeverity.error
-                pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
-                data     := s!"You are not allowed to use the tactic '{forbiddenTac}'"
-              }
-            }
+          findForbiddenTactics inputCtx level tacticStx
 
           -- Insert invisible `skip` command to make sure we always display the initial goal
           let skip := Syntax.node (.original default 0 default endOfWhitespace) ``Lean.Parser.Tactic.skip #[]
diff --git a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
index c49767b..614490b 100644
--- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
@@ -28,3 +28,4 @@ HiddenHint : 42 = 42 =>
 Conclusion "Bravo! PS: `rfl` steht für \"reflexivity\"."
 
 NewTactics rfl
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
index b11bee5..754aae9 100644
--- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
@@ -33,3 +33,4 @@ HiddenHint (n : ℕ) (h : 1 < n) : 1 < n =>
 Conclusion ""
 
 NewTactics assumption
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
index 9940e83..a8ff296 100644
--- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
@@ -28,3 +28,4 @@ HiddenHint (A : Prop) (hA : A) : A =>
 Conclusion ""
 
 NewTactics assumption
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L04_True.lean b/server/testgame/TestGame/Levels/Proposition/L04_True.lean
index 11cf084..352ce3e 100644
--- a/server/testgame/TestGame/Levels/Proposition/L04_True.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L04_True.lean
@@ -34,3 +34,4 @@ True := by
 Conclusion ""
 
 NewTactics trivial
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
index 52c7bea..1030b90 100644
--- a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
@@ -22,3 +22,4 @@ Statement
 Conclusion ""
 
 NewTactics trivial
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L06_False.lean b/server/testgame/TestGame/Levels/Proposition/L06_False.lean
index 5a4dad2..b81feb4 100644
--- a/server/testgame/TestGame/Levels/Proposition/L06_False.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L06_False.lean
@@ -28,3 +28,4 @@ HiddenHint (A : Prop) (h : False) : A =>
 unabhängig davon, was das Goal ist."
 
 NewTactics contradiction
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
index 92bf991..d2d6309 100644
--- a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
@@ -27,3 +27,4 @@ Conclusion
 "
 
 NewTactics contradiction
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
index ad48dca..dca804b 100644
--- a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
@@ -30,3 +30,4 @@ Conclusion
 "
 
 NewTactics contradiction
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L09_And.lean b/server/testgame/TestGame/Levels/Proposition/L09_And.lean
index 981ef87..9aa3f37 100644
--- a/server/testgame/TestGame/Levels/Proposition/L09_And.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L09_And.lean
@@ -33,6 +33,7 @@ HiddenHint (A : Prop) (hA : A) : A =>
   "Du hast einen Beweis dafür in den *Annahmen*."
 
 NewTactics constructor assumption
+DisabledTactics tauto
 
 -- Statement
 --     "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$."
diff --git a/server/testgame/TestGame/Levels/Proposition/L10_And.lean b/server/testgame/TestGame/Levels/Proposition/L10_And.lean
index 79988f4..6579ff7 100644
--- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean
@@ -34,6 +34,7 @@ HiddenHint (A : Prop) (hA : A) : A =>
   "Du hast einen Beweis dafür in den *Annahmen*."
 
 NewTactics constructor assumption
+DisabledTactics tauto
 
 -- Statement
 --     "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$."
diff --git a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
index e85ba8b..deeb72e 100644
--- a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
@@ -31,3 +31,4 @@ Hint (A : Prop) (B : Prop) (hA : A) : ¬ B =>
 "Sackgasse. Probier's nochmals."
 
 NewTactics left right assumption
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
index b42f944..272dc84 100644
--- a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
@@ -45,3 +45,4 @@ Hint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
 "Jetzt noch das UND in den Annahmen mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
 
 NewTactics assumption rcases
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
index d4d7c82..00f1f86 100644
--- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
@@ -123,3 +123,4 @@ HiddenHint (A : Prop) (B : Prop) : A ∨ B =>
 "`left` oder `right`?"
 
 NewTactics left right assumption constructor rcases rfl contradiction trivial
+DisabledTactics tauto