diff --git a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean index 0f18dc5..0e5788a 100644 --- a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean +++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean @@ -32,7 +32,7 @@ Gerade seid Ihr auf Königin Logisindes Planeten. Sie kommt ohne Umschweife zum **Logisinde** Werte Wesen aus fremden Welten, gestatten Sie eine Frage. Warum gilt … -Und er kritzelt etwas auf ein Stück Papier: oben ein paar Annahmen, unten eine Schlussfolgerung. +Und sie kritzelt etwas auf ein Stück Papier: oben ein paar Annahmen, unten eine Schlussfolgerung. Dazwischen sollst Du offenbar einen Beweis eintragen. Du siehst Robo hilflos an. " @@ -44,7 +44,7 @@ Statement "" Hint (A B C : Prop) : ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) => - "**Robo** Das ist ganz einfach. Mit `A B C : Prop` meint er: `A`, `B` und `C` sind irgendwelche Aussagen (*propositions*). Und mit `→` meint er ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder? + "**Robo** Das ist ganz einfach. Mit `A B C : Prop` meint sie: `A`, `B` und `C` sind irgendwelche Aussagen (*propositions*). Und mit `→` meint sie ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder? **Du** Ehhm, ja. Aber da muss ich jetzt trotzdem erst einmal überlegen. diff --git a/server/testgame/TestGame/Levels/Proposition/L06_False.lean b/server/testgame/TestGame/Levels/Proposition/L06_False.lean index 51855ae..519b018 100644 --- a/server/testgame/TestGame/Levels/Proposition/L06_False.lean +++ b/server/testgame/TestGame/Levels/Proposition/L06_False.lean @@ -6,7 +6,7 @@ Game "TestGame" World "Proposition" Level 7 -Title "Widerspruch beweist alles." +Title "Aus Falschem folgt vieles." Introduction " diff --git a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean index 81d3627..0eee982 100644 --- a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean +++ b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean @@ -8,7 +8,7 @@ Game "TestGame" World "Proposition" Level 8 -Title "Widerspruch" +Title "Aus Falschem folgt vieles." Introduction " diff --git a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean index 40190cf..e43bf5f 100644 --- a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean +++ b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean @@ -8,7 +8,7 @@ Game "TestGame" World "Proposition" Level 9 -Title "Widerspruch" +Title "Aus Falschem folgt vieles." Introduction " diff --git a/server/testgame/TestGame/Levels/Proposition/L10_And.lean b/server/testgame/TestGame/Levels/Proposition/L10_And.lean index 68bfe13..8c042f3 100644 --- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean @@ -11,7 +11,7 @@ Title "Und" Introduction " -Langsam wird die Schlange kürzer. Die nächste Formalosophin hat folgendes Anliegen: +Langsam wird die Schlange kürzer. Die nächste Formalosophin, ebenfalls häkelnd, hat folgendes Anliegen. " Statement ""