From 874999ed34482fd2e43caa6916b80ca225b3efe3 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Mon, 6 Mar 2023 10:19:45 +0100
Subject: [PATCH] show summary permanently

---
 .../Levels/Proposition/L13_Summary.lean         | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
index 32879ce..d5d7826 100644
--- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
@@ -13,6 +13,13 @@ Title "Zusammenfassung"
 Introduction
 "
 Der letzte Untertan tritt vor.  Ihr Anliegen ist etwas komplizierter als die vorherigen.
+
+**Robo** Wirf einfach alles drauf, was Du gelernt hast.  Hier, ich bin sogar so nett und zeig Dir noch einmal die vier wichtigsten Taktiken für diese Situation an.
+
+| (Übersicht) | Und (`∧`)                | Oder (`∨`)              |
+|-------------|:-------------------------|:------------------------|
+| Annahme     | `rcases h with ⟨h₁, h₂⟩` | `rcases h with h \\| h` |
+| Goal        | `constructor`            | `left`/`right`          |
 "
 
 -- Note: The other direction would need arguing by cases.
@@ -33,16 +40,6 @@ Statement ""
   right
   assumption
 
-Hint (A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) =>
-"
-**Robo** Wirf einfach alles drauf, was Du gelernt hast.  Hier, ich bin sogar so nett und zeig Dir noch einmal die beiden vier wichtigsten Taktiken für diese Situation an.
-
-| (Übersicht) | Und (`∧`)                | Oder (`∨`)              |
-|-------------|:-------------------------|:------------------------|
-| Annahme     | `rcases h with ⟨h₁, h₂⟩` | `rcases h with h \\| h` |
-| Goal        | `constructor`            | `left`/`right`          |
-"
-
 HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) =>
 "**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."