diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index 57712a3..f211b1c 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -190,16 +190,8 @@ instance : Quote TacticDocEntry `term :=
 /-- Declare the list of tactics that will be displayed in the current level.
 Expects a space separated list of identifiers that refer to either a tactic doc
 entry or a tactic doc set. -/
-elab "Tactics" args:ident* : command => do
-  let env ← getEnv
-  let docs := tacticDocExt.getState env
-  let mut tactics : Array TacticDocEntry := #[]
-  for arg in args do
-    let name := arg.getId
-    match docs.find? (·.name = name) with
-    | some entry => tactics := tactics.push entry
-    | none => throwError "Tactic doc {name} wasn't found."
-  modifyCurLevel fun level => pure {level with tactics := tactics}
+elab "NewTactics" args:ident* : command => do
+  modifyCurLevel fun level => pure {level with newTactics := args.map (·.getId)}
 
 /-! ## Lemmas -/
 
@@ -219,11 +211,11 @@ Expect an identifier used as the set name then `:=` and a
 space separated list of identifiers. -/
 elab "LemmaSet" name:ident ":" title:str ":=" args:ident* : command => do
   let docs := lemmaDocExt.getState (← getEnv)
-  let mut entries : Array LemmaDocEntry := #[]
+  let mut entries : Array Name := #[]
   for arg in args do
     let name := arg.getId
     match docs.find? (·.userName = name) with
-    | some doc => entries := entries.push doc
+    | some doc => entries := entries.push name
     | none => throwError "Lemma doc {name} wasn't found."
   modifyEnv (lemmaSetExt.addEntry · {
     name := name.getId,
@@ -236,16 +228,60 @@ instance : Quote LemmaDocEntry `term :=
 /-- Declare the list of lemmas that will be displayed in the current level.
 Expects a space separated list of identifiers that refer to either a lemma doc
 entry or a lemma doc set. -/
-elab "Lemmas" args:ident* : command => do
+elab "NewLemmas" args:ident* : command => do
   let env ← getEnv
   let docs := lemmaDocExt.getState env
   let sets := lemmaSetExt.getState env
-  let mut lemmas : Array LemmaDocEntry := #[]
+  let mut lemmas : Array Name := #[]
   for arg in args do
     let name := arg.getId
     match docs.find? (·.userName = name) with
-    | some entry => lemmas := lemmas.push entry
+    | some entry => lemmas := lemmas.push name
     | none => match sets.find? (·.name = name) with
               | some entry => lemmas := lemmas ++ entry.lemmas
               | none => throwError "Lemma doc or lemma set {name} wasn't found."
-  modifyCurLevel fun level => pure {level with lemmas := lemmas}
+  modifyCurLevel fun level => pure {level with newLemmas := lemmas}
+
+/-! ## Make Game -/
+
+def getTacticDoc! (tac : Name) : CommandElabM TacticDocEntry := do
+  match (tacticDocExt.getState (← getEnv)).find? (·.name = tac) with
+  | some doc => return doc
+  | none => throwError "Tactic documentation not found: {tac}"
+
+/-- Make the final Game. This command will precompute various things about the game, such as which
+tactics are available in each level etc. -/
+elab "MakeGame" : command => do
+  let game ← getCurGame
+
+  -- Check for loops in world graph
+  if game.worlds.hasLoops then
+    throwError "World graph has loops!"
+
+  -- Compute which tactics are available in which level:
+  let mut newTacticsInWorld : HashMap Name (HashSet Name) := {}
+  for (worldId, world) in game.worlds.nodes.toArray do
+    let mut newTactics : HashSet Name:= {}
+    for (_, level) in world.levels.toArray do
+      newTactics := newTactics.insertMany level.newTactics
+    newTacticsInWorld := newTacticsInWorld.insert worldId newTactics
+
+  let mut tacticsInWorld : HashMap Name (HashSet Name) := {}
+  for (worldId, _) in game.worlds.nodes.toArray do
+    let mut tactics : HashSet Name:= {}
+    let predecessors := game.worlds.predecessors worldId
+    for predWorldId in predecessors do
+      tactics := tactics.insertMany (newTacticsInWorld.find! predWorldId)
+    tacticsInWorld := tacticsInWorld.insert worldId tactics
+
+  for (worldId, world) in game.worlds.nodes.toArray do
+    let mut tactics := tacticsInWorld.find! worldId
+    logInfo m!"{tactics.toArray}"
+
+    let levels := world.levels.toArray.insertionSort fun a b => a.1 < b.1
+
+    for (levelId, level) in levels do
+      tactics := tactics.insertMany level.newTactics
+
+      modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
+        return {level with tactics := ← tactics.toArray.mapM getTacticDoc!}
diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean
index fb4ab8a..6e726f5 100644
--- a/server/leanserver/GameServer/EnvExtensions.lean
+++ b/server/leanserver/GameServer/EnvExtensions.lean
@@ -1,4 +1,6 @@
 import Lean
+import GameServer.Graph
+
 /-! # Environment extensions
 
 The game framework stores almost all its game building data in environment extensions
@@ -71,7 +73,7 @@ elab "#print_lemma_doc" : command => do
 structure LemmaSetEntry where
   name : Name
   title : String
-  lemmas : Array LemmaDocEntry
+  lemmas : Array Name
   deriving ToJson, Repr
 
 /-- Environment extension for lemma sets. -/
@@ -86,26 +88,8 @@ open Elab Command in
 /-- Print all registered lemma sets for debugging purposes. -/
 elab "#print_lemma_set" : command => do
   for entry in lemmaSetExt.getState (← getEnv) do
-    dbg_trace "{entry.name} : {entry.lemmas.map LemmaDocEntry.name}"
-
-/-! ## Graph -/
-
-structure Graph (α β : Type) [inst : BEq α] [inst : Hashable α] where
-  nodes: HashMap α β := {}
-  edges: Array (α × α) := {}
-deriving Inhabited
-
-instance [ToJson β] : ToJson (Graph Name β) := {
-  toJson := fun graph => Json.mkObj [
-    ("nodes", Json.mkObj (graph.nodes.toList.map fun (a,b) => (a.toString, toJson b))),
-    ("edges", toJson graph.edges)
-  ]
-}
-
-instance [inst : BEq α] [inst : Hashable α] : EmptyCollection (Graph α β) := ⟨default⟩
+    dbg_trace "{entry.name} : {entry.lemmas}"
 
-def Graph.insertNode [inst : BEq α] [inst : Hashable α] (g : Graph α β) (a : α) (b : β) :=
-  {g with nodes := g.nodes.insert a b}
 
 /-! ## Environment extensions for game specification-/
 
@@ -179,7 +163,21 @@ structure GameLevel where
   introduction: String := default
   description: String := default
   conclusion: String := default
+  -- new tactics introduces by this level:
+  newTactics: Array Name := default
+  -- tactics exceptionally forbidden in this level:
+  disabledTactics: Array Name := default
+  -- only these tactics are allowed in this level (ignore if empty):
+  onlyTactics: Array Name := default
+  -- tactics in this level (computed by `MakeGame`):
   tactics: Array TacticDocEntry := default
+  -- new lemmas introduces by this level:
+  newLemmas: Array Name := default
+  -- lemmas exceptionally forbidden in this level:
+  disabledLemmas: Array Name := default
+  -- only these lemmas are allowed in this level (ignore if empty):
+  onlyLemmas: Array Name := default
+  -- lemmas in this level (computed by `MakeGame`):
   lemmas: Array LemmaDocEntry := default
   hints: Array GoalHintEntry := default
   goal : TSyntax `Lean.Parser.Command.declSig := default
@@ -310,3 +308,15 @@ def modifyCurLevel (fn : GameLevel → m GameLevel) [MonadError m] : m Unit := d
   modifyCurWorld fun world => do
     let level ← getCurLevel
     return {world with levels := world.levels.insert level.index (← fn level)}
+
+def modifyLevel (levelId : LevelId) (fn : GameLevel → m GameLevel) [MonadError m] : m Unit := do
+  let some game ← getGame? levelId.game
+    | throwError m!"Game {levelId.game} does not exist"
+  let some world := (← getCurGame).worlds.nodes.find? levelId.world
+    | throwError m!"World {levelId.world} does not exist"
+  let some level := world.levels.find? levelId.level
+    | throwError m!"Level {levelId.level} does not exist"
+  let level' ← fn level
+  let world' := {world with levels := world.levels.insert levelId.level level'}
+  let game' := {game with worlds := game.worlds.insertNode levelId.world world'}
+  insertGame levelId.game game'
diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean
index 246233a..eacf2ca 100644
--- a/server/testgame/TestGame.lean
+++ b/server/testgame/TestGame.lean
@@ -39,9 +39,12 @@ Conclusion
 
 
 Path Proposition → Implication → Predicate → Contradiction → LeanStuff
---Path Predicate → Prime
+-- Path Predicate → Prime
 Path Predicate → Induction → LeanStuff → Function → SetFunction
 
 Path LeanStuff → SetTheory → SetFunction
 
 Path SetTheory → SetTheory2
+
+
+MakeGame
diff --git a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean
index 467ffee..b4b4ddf 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean
@@ -63,6 +63,6 @@ have k : ¬ B
 
 Conclusion ""
 
-Tactics contradiction rcases haveₓ assumption apply
+NewTactics contradiction rcases haveₓ assumption apply
 
-Lemmas Even Odd not_even not_odd
+NewLemmas Even Odd not_even not_odd
diff --git a/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean
index 29e586e..4f36b7a 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean
@@ -60,6 +60,6 @@ Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False =>
 
 Conclusion ""
 
-Tactics contradiction apply assumption rcases sufficesₓ
+NewTactics contradiction apply assumption rcases sufficesₓ
 
-Lemmas Even Odd not_even not_odd
+NewLemmas Even Odd not_even not_odd
diff --git a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean
index 17fadbf..50a5246 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean
@@ -52,4 +52,4 @@ HiddenHint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False =>
 
 Conclusion ""
 
-Tactics by_contra sufficesₓ haveₓ contradiction apply assumption
+NewTactics by_contra sufficesₓ haveₓ contradiction apply assumption
diff --git a/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean
index c4d44df..d3cbe73 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean
@@ -46,4 +46,4 @@ HiddenHint (A : Prop) (B : Prop) : A → B ↔ (¬ B → ¬ A) =>
 
 Conclusion ""
 
-Tactics contradiction constructor intro by_contra sufficesₓ haveₓ apply assumption
+NewTactics contradiction constructor intro by_contra sufficesₓ haveₓ apply assumption
diff --git a/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean b/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean
index ed3f32d..cec04e7 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean
@@ -61,5 +61,5 @@ Hint (n : ℕ) : Even n → ¬Odd (n ^ 2) =>
 Hint (n : ℕ) : Even n → Even (n ^ 2) =>
 "Diese Aussage hast du bereits als Lemma bewiesen, schau mal in der Bibliothek."
 
-Tactics contrapose rw apply
-Lemmas Even Odd not_even not_odd even_square
+NewTactics contrapose rw apply
+NewLemmas Even Odd not_even not_odd even_square
diff --git a/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean
index 20dc4ac..d700e70 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean
@@ -71,6 +71,6 @@ HiddenHint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) =>
 "Probiers mit `apply ...`"
 
 
-Tactics contradiction by_contra rw apply assumption -- TODO: suffices, have
+NewTactics contradiction by_contra rw apply assumption -- TODO: suffices, have
 
-Lemmas Odd Even not_odd not_even even_square
+NewLemmas Odd Even not_odd not_even even_square
diff --git a/server/testgame/TestGame/Levels/Function/L01_xxx.lean b/server/testgame/TestGame/Levels/Function/L01_xxx.lean
index 651b853..4048f5a 100644
--- a/server/testgame/TestGame/Levels/Function/L01_xxx.lean
+++ b/server/testgame/TestGame/Levels/Function/L01_xxx.lean
@@ -23,4 +23,4 @@ Statement
     : True := by
   trivial
 
-Tactics rw
+NewTactics rw
diff --git a/server/testgame/TestGame/Levels/Implication/L01_Intro.lean b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean
index d5735cf..292005b 100644
--- a/server/testgame/TestGame/Levels/Implication/L01_Intro.lean
+++ b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean
@@ -37,4 +37,4 @@ HiddenHint (A : Prop) (B : Prop) (hb : B) : A → (A ∧ B) =>
 Hint (A : Prop) (B : Prop) (ha : A) (hb : B) : (A ∧ B) =>
 "Jetzt kannst du die Taktiken aus dem letzten Kapitel verwenden."
 
-Tactics intro constructor assumption
+NewTactics intro constructor assumption
diff --git a/server/testgame/TestGame/Levels/Implication/L02_Revert.lean b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean
index e76d7eb..74452a8 100644
--- a/server/testgame/TestGame/Levels/Implication/L02_Revert.lean
+++ b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean
@@ -39,4 +39,4 @@ dass $B$ wahr ist."
 HiddenHint (A : Prop) (B : Prop) (ha : A) (h : A → B): B =>
 "Mit `revert ha` kann man die Annahme `ha` als Implikationsprämisse vorne ans Goal anhängen."
 
-Tactics revert assumption
+NewTactics revert assumption
diff --git a/server/testgame/TestGame/Levels/Implication/L03_Apply.lean b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean
index 7727721..71272b2 100644
--- a/server/testgame/TestGame/Levels/Implication/L03_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean
@@ -32,7 +32,7 @@ HiddenHint (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
 "Nachdem du die Implikation `A → B` angewendet hast, musst du nur noch $A$ zeigen,
 dafür hast du bereits einen Beweis in den Annahmen."
 
-Tactics apply assumption
+NewTactics apply assumption
 
 -- Katex notes
 -- `\\(    \\)` or `$   $` for inline
diff --git a/server/testgame/TestGame/Levels/Implication/L04_Apply.lean b/server/testgame/TestGame/Levels/Implication/L04_Apply.lean
index 7d18abc..e227720 100644
--- a/server/testgame/TestGame/Levels/Implication/L04_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L04_Apply.lean
@@ -32,4 +32,4 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C)
 "Du willst $C$ beweisen. Suche also nach einer Implikation $\\ldots \\Rightarrow C$ und wende
 diese mit `apply` an."
 
-Tactics intro apply assumption revert
+NewTactics intro apply assumption revert
diff --git a/server/testgame/TestGame/Levels/Implication/L05_Apply.lean b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean
index 155127c..83292a5 100644
--- a/server/testgame/TestGame/Levels/Implication/L05_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean
@@ -48,6 +48,6 @@ Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
     (i : D → E) (k : E → F) (m : C → F) : D =>
 "Sackgasse. Probier doch einen anderen Weg."
 
-Tactics apply assumption revert intro
+NewTactics apply assumption revert intro
 
 -- https://www.jmilne.org/not/Mamscd.pdf
diff --git a/server/testgame/TestGame/Levels/Implication/L06_Iff.lean b/server/testgame/TestGame/Levels/Implication/L06_Iff.lean
index 54b93c8..dee2b57 100644
--- a/server/testgame/TestGame/Levels/Implication/L06_Iff.lean
+++ b/server/testgame/TestGame/Levels/Implication/L06_Iff.lean
@@ -38,6 +38,6 @@ aus mehreren Einzelteilen besteht: `⟨A → B, B → A⟩`. Man sagt also Lean,
 ob das Goal aus solchen Einzelteilen \"konstruiert\" werden kann.
 "
 
-Tactics constructor assumption
+NewTactics constructor assumption
 
 -- TODO : `case mpr =>` ist mathematisch noch sinnvoll.
diff --git a/server/testgame/TestGame/Levels/Implication/L07_Rw.lean b/server/testgame/TestGame/Levels/Implication/L07_Rw.lean
index 93d67bd..17ca7d9 100644
--- a/server/testgame/TestGame/Levels/Implication/L07_Rw.lean
+++ b/server/testgame/TestGame/Levels/Implication/L07_Rw.lean
@@ -71,4 +71,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔
 "Das ist nicht der optimale Weg..."
 
 
-Tactics rw assumption
+NewTactics rw assumption
diff --git a/server/testgame/TestGame/Levels/Implication/L08_Iff.lean b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean
index d0cabaf..0bf64f0 100644
--- a/server/testgame/TestGame/Levels/Implication/L08_Iff.lean
+++ b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean
@@ -41,4 +41,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B =
 
 Conclusion "Im nächsten Level findest du die zweite Option."
 
-Tactics apply assumption
+NewTactics apply assumption
diff --git a/server/testgame/TestGame/Levels/Implication/L09_Iff.lean b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean
index 41f7c4f..a3c6fe2 100644
--- a/server/testgame/TestGame/Levels/Implication/L09_Iff.lean
+++ b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean
@@ -36,7 +36,7 @@ Conclusion
 "
 "
 
-Tactics intro apply rcases assumption
+NewTactics intro apply rcases assumption
 
 -- -- TODO: The new `cases` works differntly. There is also `cases'`
 -- example (A B : Prop) : (A ↔ B) → (A → B) := by
diff --git a/server/testgame/TestGame/Levels/Implication/L10_Apply.lean b/server/testgame/TestGame/Levels/Implication/L10_Apply.lean
index 4b57f5c..4bea8e4 100644
--- a/server/testgame/TestGame/Levels/Implication/L10_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L10_Apply.lean
@@ -50,6 +50,6 @@ Conclusion
 "
 "
 
-Tactics apply left right assumption
+NewTactics apply left right assumption
 
-Lemmas not_or_of_imp
+NewLemmas not_or_of_imp
diff --git a/server/testgame/TestGame/Levels/Implication/L11_Rw.lean b/server/testgame/TestGame/Levels/Implication/L11_Rw.lean
index 6370dc9..1151fb4 100644
--- a/server/testgame/TestGame/Levels/Implication/L11_Rw.lean
+++ b/server/testgame/TestGame/Levels/Implication/L11_Rw.lean
@@ -34,6 +34,6 @@ Conclusion
 `rw` hat automatisch `rfl` ausgeführt und dadurch den Beweis beendet.
 "
 
-Tactics rw
+NewTactics rw
 
-Lemmas not_not not_or_of_imp
+NewLemmas not_not not_or_of_imp
diff --git a/server/testgame/TestGame/Levels/Implication/L12_Summary.lean b/server/testgame/TestGame/Levels/Implication/L12_Summary.lean
index 6569583..7a64ade 100644
--- a/server/testgame/TestGame/Levels/Implication/L12_Summary.lean
+++ b/server/testgame/TestGame/Levels/Implication/L12_Summary.lean
@@ -76,6 +76,6 @@ HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) (ha : A) : B =>
 HiddenHint (A : Prop) (B: Prop) (ha : A) (ha' : ¬A) : B =>
 "Findest du einen Widerspruch?"
 
-Tactics rfl assumption trivial left right constructor rcases
+NewTactics rfl assumption trivial left right constructor rcases
 
-Lemmas not_not not_or_of_imp
+NewLemmas not_not not_or_of_imp
diff --git a/server/testgame/TestGame/Levels/Induction/L01_Simp.lean b/server/testgame/TestGame/Levels/Induction/L01_Simp.lean
index 8eef726..f1fd429 100644
--- a/server/testgame/TestGame/Levels/Induction/L01_Simp.lean
+++ b/server/testgame/TestGame/Levels/Induction/L01_Simp.lean
@@ -43,4 +43,4 @@ Statement
     (n : ℕ) : (∑ i : Fin n, (0 + 0)) = 0 := by
   simp
 
-Tactics simp
+NewTactics simp
diff --git a/server/testgame/TestGame/Levels/Induction/L02_Sum.lean b/server/testgame/TestGame/Levels/Induction/L02_Sum.lean
index 224ec3c..646dccd 100644
--- a/server/testgame/TestGame/Levels/Induction/L02_Sum.lean
+++ b/server/testgame/TestGame/Levels/Induction/L02_Sum.lean
@@ -34,4 +34,4 @@ Statement
   simp
   ring
 
-Tactics rw simp ring
+NewTactics rw simp ring
diff --git a/server/testgame/TestGame/Levels/Induction/L03_Induction.lean b/server/testgame/TestGame/Levels/Induction/L03_Induction.lean
index 108c0a8..accd7b9 100644
--- a/server/testgame/TestGame/Levels/Induction/L03_Induction.lean
+++ b/server/testgame/TestGame/Levels/Induction/L03_Induction.lean
@@ -43,4 +43,4 @@ Statement
   -- rw [mul_add, hn]
   -- ring
 
-Tactics ring
+NewTactics ring
diff --git a/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean b/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean
index e796abd..5deac8c 100644
--- a/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean
+++ b/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean
@@ -30,4 +30,4 @@ $\\sum_{i = 0}^n (2n + 1) = n ^ 2$."
   --rw [hn]
   --ring
 
-Tactics ring
+NewTactics ring
diff --git a/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean b/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean
index 02e4c0b..876b75c 100644
--- a/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean
+++ b/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean
@@ -44,4 +44,4 @@ Statement
   -- rw [mul_add, hn]
   -- ring
 
-Tactics ring
+NewTactics ring
diff --git a/server/testgame/TestGame/Levels/Induction/T00_Sum.lean b/server/testgame/TestGame/Levels/Induction/T00_Sum.lean
index be78477..dce7bf2 100644
--- a/server/testgame/TestGame/Levels/Induction/T00_Sum.lean
+++ b/server/testgame/TestGame/Levels/Induction/T00_Sum.lean
@@ -23,4 +23,4 @@ Statement
   simp
   sorry
 
-Tactics ring
+NewTactics ring
diff --git a/server/testgame/TestGame/Levels/Induction/T01_Induction.lean b/server/testgame/TestGame/Levels/Induction/T01_Induction.lean
index 2197ebe..05ab14f 100644
--- a/server/testgame/TestGame/Levels/Induction/T01_Induction.lean
+++ b/server/testgame/TestGame/Levels/Induction/T01_Induction.lean
@@ -21,4 +21,4 @@ Statement
     (n : ℕ) : True := by
   sorry
 
-Tactics rw simp ring
+NewTactics rw simp ring
diff --git a/server/testgame/TestGame/Levels/Induction/T02_Induction.lean b/server/testgame/TestGame/Levels/Induction/T02_Induction.lean
index cc0d2dd..5041403 100644
--- a/server/testgame/TestGame/Levels/Induction/T02_Induction.lean
+++ b/server/testgame/TestGame/Levels/Induction/T02_Induction.lean
@@ -21,4 +21,4 @@ Statement
     (n : ℤ) : True := by
   sorry
 
-Tactics rw simp ring
+NewTactics rw simp ring
diff --git a/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean b/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean
index f23163b..96e789f 100644
--- a/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean
+++ b/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean
@@ -21,7 +21,7 @@ Statement
     (n : ℕ) : True := by
   trivial
 
-Tactics simp
+NewTactics simp
 
 
 -- Σ_i Σ_j ... = Σ_j Σ_i ...
diff --git a/server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean b/server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean
index e7b21c8..f46dbdb 100644
--- a/server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean
+++ b/server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean
@@ -29,4 +29,4 @@ Statement
     "TODO" : True := by
   trivial
 
-Tactics rw
+NewTactics rw
diff --git a/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean b/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean
index 17930a8..e6f93aa 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean
@@ -67,4 +67,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C ∧ A =>
 Hint (A : Prop) (B : Prop) (C : Prop) (h : A → C) : C ∧ A =>
 "Ein UND im Goal kann mit `constructor` aufgeteilt werden."
 
-Tactics left right assumption constructor rcases
+NewTactics left right assumption constructor rcases
diff --git a/server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean b/server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean
index acce168..ba06057 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean
@@ -20,4 +20,4 @@ Conclusion
 "
 "
 
-Tactics ring
+NewTactics ring
diff --git a/server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean b/server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean
index de45f47..ce83d69 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean
@@ -20,4 +20,4 @@ Conclusion
 "
 "
 
-Tactics ring
+NewTactics ring
diff --git a/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean b/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean
index b0f6232..610ec64 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean
@@ -58,4 +58,4 @@ Hint (n : ℕ) (hn : odd n) (h : ∀ (x : ℕ), (odd x) → even (x + 1)) : even
 "`∀ (x : ℕ), (odd x) → even (x + 1)` ist eigentlich das gleiche wie
 `(x : ℕ) → `"
 
-Tactics ring intro unfold
+NewTactics ring intro unfold
diff --git a/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean b/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean
index 84c8044..129c126 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean
@@ -22,4 +22,4 @@ Statement : ∃ (f : ℕ → ℕ), ∀ (x : ℕ), f x = 0 := by
 
 Conclusion ""
 
-Tactics use simp
+NewTactics use simp
diff --git a/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean
index 31c3006..52d5908 100644
--- a/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean
@@ -39,6 +39,6 @@ Ring zu lösen, funktioniert aber auch auf `ℕ`, auch wenn dieses kein Ring ist
 (erst `ℤ` ist ein Ring).
 "
 
-Tactics ring
+NewTactics ring
 
 #eval 4 / 6
diff --git a/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean
index 22ee139..9e8f068 100644
--- a/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean
@@ -67,4 +67,4 @@ Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃
 
 Conclusion "Übrigens, mit `rw [h₁, ←h₂]` könnte man mehrere `rw` zusammenfassen."
 
-Tactics assumption rw
+NewTactics assumption rw
diff --git a/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean
index 2395208..2320b54 100644
--- a/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean
@@ -37,4 +37,4 @@ Hint (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : a + a ^ 2 = a + 1
 Conclusion "Übrigens, mit `rw [h] at *` kann man im weiteren `h` in **allen** Annahmen und
 dem Goal umschreiben."
 
-Tactics assumption rw
+NewTactics assumption rw
diff --git a/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean
index 42460c2..3d1f19d 100644
--- a/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean
@@ -30,4 +30,4 @@ Hint (y : ℕ) : (2 * y + 1) ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y =>
 
 Conclusion ""
 
-Tactics ring rw
+NewTactics ring rw
diff --git a/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean b/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean
index 73a940f..32ecad3 100644
--- a/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean
@@ -28,4 +28,4 @@ Conclusion
 aufzurufen, deshalb brauchst du das nur noch selten.
 "
 
-Tactics rfl
+NewTactics rfl
diff --git a/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean b/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
index 8bbcd67..9ae29ce 100644
--- a/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
@@ -67,5 +67,5 @@ Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : n ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
 Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
 "Die Taktik `ring` löst solche Gleichungen."
 
-Tactics unfold rcases use rw ring
-Lemmas Even Odd
+NewTactics unfold rcases use rw ring
+NewLemmas Even Odd
diff --git a/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean b/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean
index 9d6af52..5e1b812 100644
--- a/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean
@@ -50,4 +50,4 @@ Hint (n : ℕ) (hn : Odd n) (h : ∀ (x : ℕ), (Odd x) → Even (x + 1)) : Even
 Conclusion "Für-alle-Statements, Implikationen und Lemmas/Theoreme verhalten sich alle
 praktisch gleich. Mehr dazu später."
 
-Tactics ring intro unfold
+NewTactics ring intro unfold
diff --git a/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean b/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean
index 306dd9e..24f03a5 100644
--- a/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean
@@ -62,6 +62,6 @@ Hint (n : ℕ) : n + n = 2 * n => "Recap: `ring` löst Gleichungen in `ℕ`."
 
 Conclusion ""
 
-Tactics push_neg intro use rw unfold ring
+NewTactics push_neg intro use rw unfold ring
 
-Lemmas Even Odd not_even not_odd not_exists not_forall
+NewLemmas Even Odd not_even not_odd not_exists not_forall
diff --git a/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean b/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean
index 0ba22c4..00f7730 100644
--- a/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean
@@ -50,6 +50,6 @@ Statement
 
 Conclusion ""
 
-Tactics push_neg intro use rw unfold ring
+NewTactics push_neg intro use rw unfold ring
 
-Lemmas Even Odd not_even not_odd not_exists not_forall
+NewLemmas Even Odd not_even not_odd not_exists not_forall
diff --git a/server/testgame/TestGame/Levels/Prime/L01_Prime.lean b/server/testgame/TestGame/Levels/Prime/L01_Prime.lean
index b6ae747..3ee93e4 100644
--- a/server/testgame/TestGame/Levels/Prime/L01_Prime.lean
+++ b/server/testgame/TestGame/Levels/Prime/L01_Prime.lean
@@ -34,6 +34,6 @@ Statement
 
 Conclusion ""
 
-Tactics
+NewTactics
 
-Lemmas
+NewLemmas
diff --git a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
index 5824a91..4c09230 100644
--- a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
@@ -48,4 +48,4 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop): ¬((¬B ∨ ¬ C) ∨ (A → B)) 
 
 Conclusion ""
 
-Tactics tauto
+NewTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
index 2171491..c49767b 100644
--- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
@@ -27,4 +27,4 @@ HiddenHint : 42 = 42 =>
 
 Conclusion "Bravo! PS: `rfl` steht für \"reflexivity\"."
 
-Tactics rfl
+NewTactics rfl
diff --git a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
index 21fb31f..b11bee5 100644
--- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
@@ -32,4 +32,4 @@ HiddenHint (n : ℕ) (h : 1 < n) : 1 < n =>
 
 Conclusion ""
 
-Tactics assumption
+NewTactics assumption
diff --git a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
index bb038f2..9940e83 100644
--- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
@@ -27,4 +27,4 @@ HiddenHint (A : Prop) (hA : A) : A =>
 
 Conclusion ""
 
-Tactics assumption
+NewTactics assumption
diff --git a/server/testgame/TestGame/Levels/Proposition/L04_True.lean b/server/testgame/TestGame/Levels/Proposition/L04_True.lean
index bbbac31..11cf084 100644
--- a/server/testgame/TestGame/Levels/Proposition/L04_True.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L04_True.lean
@@ -33,4 +33,4 @@ True := by
 
 Conclusion ""
 
-Tactics trivial
+NewTactics trivial
diff --git a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
index 0aaf9df..52c7bea 100644
--- a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
@@ -21,4 +21,4 @@ Statement
 
 Conclusion ""
 
-Tactics trivial
+NewTactics trivial
diff --git a/server/testgame/TestGame/Levels/Proposition/L06_False.lean b/server/testgame/TestGame/Levels/Proposition/L06_False.lean
index 990f282..5a4dad2 100644
--- a/server/testgame/TestGame/Levels/Proposition/L06_False.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L06_False.lean
@@ -27,4 +27,4 @@ HiddenHint (A : Prop) (h : False) : A =>
 "Wenn man einen Beweis von `False` hat, kann man mit `contradiction` das Goal beweisen,
 unabhängig davon, was das Goal ist."
 
-Tactics contradiction
+NewTactics contradiction
diff --git a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
index 286dbc1..92bf991 100644
--- a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
@@ -26,4 +26,4 @@ Conclusion
 "
 "
 
-Tactics contradiction
+NewTactics contradiction
diff --git a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
index e2ee09f..ad48dca 100644
--- a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
@@ -29,4 +29,4 @@ Conclusion
 "
 "
 
-Tactics contradiction
+NewTactics contradiction
diff --git a/server/testgame/TestGame/Levels/Proposition/L09_And.lean b/server/testgame/TestGame/Levels/Proposition/L09_And.lean
index f33a175..981ef87 100644
--- a/server/testgame/TestGame/Levels/Proposition/L09_And.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L09_And.lean
@@ -32,7 +32,7 @@ HiddenHint (A : Prop) (B : Prop) (hA : A) (hB : B) : A ∧ B =>
 HiddenHint (A : Prop) (hA : A) : A =>
   "Du hast einen Beweis dafür in den *Annahmen*."
 
-Tactics constructor assumption
+NewTactics constructor assumption
 
 -- 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 fe85f6a..79988f4 100644
--- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean
@@ -33,7 +33,7 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ (B ∧ C)) : B =>
 HiddenHint (A : Prop) (hA : A) : A =>
   "Du hast einen Beweis dafür in den *Annahmen*."
 
-Tactics constructor assumption
+NewTactics constructor assumption
 
 -- 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 62d5147..e85ba8b 100644
--- a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
@@ -30,4 +30,4 @@ HiddenHint (A : Prop) (B : Prop) (hA : A) : A ∨ (¬ B) =>
 Hint (A : Prop) (B : Prop) (hA : A) : ¬ B =>
 "Sackgasse. Probier's nochmals."
 
-Tactics left right assumption
+NewTactics left right assumption
diff --git a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
index 984d6a6..b42f944 100644
--- a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
@@ -44,4 +44,4 @@ HiddenHint (A : Prop) (B : Prop) (h : A ∨ (A ∧ B)) : A =>
 Hint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
 "Jetzt noch das UND in den Annahmen mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
 
-Tactics assumption rcases
+NewTactics assumption rcases
diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
index b05193a..d4d7c82 100644
--- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
@@ -122,4 +122,4 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) =>
 HiddenHint (A : Prop) (B : Prop) : A ∨ B =>
 "`left` oder `right`?"
 
-Tactics left right assumption constructor rcases rfl contradiction trivial
+NewTactics left right assumption constructor rcases rfl contradiction trivial
diff --git a/server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean b/server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean
index 56fa09b..b2bf693 100644
--- a/server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean
+++ b/server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean
@@ -21,4 +21,4 @@ Statement
     : True := by
   trivial
 
-Tactics rw
+NewTactics rw
diff --git a/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean b/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean
index eb240e9..90ff1f8 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean
@@ -39,4 +39,4 @@ Statement mem_univ
   trivial
   -- tauto
 
-Tactics tauto trivial
+NewTactics tauto trivial
diff --git a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
index 483a8d3..eac4906 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
@@ -39,7 +39,7 @@ Statement subset_empty_iff
   intro h hA
   apply mem_univ -- or `trivial`.
 
-Tactics intro trivial apply
+NewTactics intro trivial apply
 -- blocked: tauto simp
 
 end MySet
diff --git a/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
index 1307805..3aeaf5c 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
@@ -54,8 +54,8 @@ Statement subset_empty_iff
   rcases a with ⟨h₁, h₂⟩
   assumption
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
 
 end MySet
diff --git a/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean b/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean
index 40260ab..c9b9908 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean
@@ -45,8 +45,8 @@ Statement eq_empty_iff_forall_not_mem
   rw [←subset_empty_iff]
   rfl -- This is quite a miracle :)
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
 
 end MySet
diff --git a/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean b/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean
index 55585e8..88e28b0 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean
@@ -30,6 +30,6 @@ Statement nonempty_iff_ne_empty
   push_neg
   rfl
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean
index 9bd7bf9..5a7a792 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean
@@ -26,6 +26,6 @@ Statement
 "" (A B : Set ℕ) : (A ∪ ∅) ∩ B = A ∩ (univ ∩ B) := by
   simp
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean
index 918313d..af7deeb 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean
@@ -30,6 +30,6 @@ Statement
   rw [←union_diff_distrib]
   rw [univ_union]
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean b/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean
index bef711c..b48d09b 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean
@@ -30,6 +30,6 @@ Statement
   rw [←not_mem_compl_iff]
   exact h4
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean b/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean
index 556d3c5..e61fcd3 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean
@@ -22,7 +22,7 @@ man die de-Morganschen Regeln einfach selber beweisen könnten.
 
 
 Die meisten Aufgaben über Mengen sind eine Kombination von `rw` und `simp_rw` verschiedenster
-Lemmas in `import Mathlib.Data.Set`.
+NewLemmas in `import Mathlib.Data.Set`.
 
 Die Taktik `simp_rw` funktioniert ähnlich wie `rw`, aber sie versucht jedes Lemma so oft
 wie möglich anzuwenden. Wir kennen also 4 etwas verwandte Optionen um Lemmas und Theoreme zu
@@ -52,7 +52,7 @@ Statement
   rw [diff_eq_compl_inter]
   rw [inter_comm]
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
 -- TODOs
 -- Lemmas compl_union compl_inter mem_compl_iff
diff --git a/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean b/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean
index dfae8fd..652584a 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean
@@ -33,6 +33,6 @@ Statement
   rw [Set.mem_diff]
   exact hx
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean b/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean
index 2501949..6b03d1b 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean
@@ -32,6 +32,6 @@ Statement
     ({4, 9} : Set ℕ) = Set.insert 4 {9} := by
   rfl
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean b/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean
index dde8c82..daf6062 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean
@@ -35,5 +35,5 @@ Statement
   simp_rw [mem_insert_iff, mem_singleton_iff] at *
   tauto
 
-Tactics simp_rw intro tauto rw
+NewTactics simp_rw intro tauto rw
 --Lemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean
index 68974a9..bc6e273 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean
@@ -32,6 +32,6 @@ Statement
   use 1
   ring
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean b/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean
index b0e2484..768f341 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean
@@ -37,6 +37,6 @@ Statement
   assumption
 
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean b/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean
index 8fe48f8..20ff5b7 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean
@@ -36,6 +36,6 @@ Statement
   ring
 
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean
index e3449fd..0887e21 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean
@@ -34,6 +34,6 @@ Statement
   ring
 
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean
index 110e17b..e98dd28 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean
@@ -28,6 +28,6 @@ Statement
     { x ∈ (S : Set ℤ) | 0 ≤ x} ⊆ S := by
   library_search
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean b/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean
index 65e8e32..2824f96 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean
@@ -23,6 +23,6 @@ Statement
   use 1
   ring
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean
index a081429..dfd5380 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean
@@ -22,6 +22,6 @@ open Set
 Statement
 "" : True := sorry
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean b/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean
index e4c74d3..7c384ad 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean
@@ -23,6 +23,6 @@ Statement
   use 1
   ring
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean b/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean
index a63620d..9b6e875 100644
--- a/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean
@@ -54,8 +54,7 @@ Statement
   rw [←Set.union_diff_distrib]
   rw [Set.univ_union]
 
-Tactics rw
-
+NewTactics rw
 
 example : 4 ∈ (univ : Set ℕ) := by
   trivial
diff --git a/server/testgame/TestGame/Levels/StatementTest.lean b/server/testgame/TestGame/Levels/StatementTest.lean
index 3ec654a..a9d47e1 100644
--- a/server/testgame/TestGame/Levels/StatementTest.lean
+++ b/server/testgame/TestGame/Levels/StatementTest.lean
@@ -35,4 +35,4 @@ lemma asdf (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c
 
 Conclusion ""
 
-Tactics assumption
+NewTactics assumption