change titles to german for now

2023-03-07 11:08:50 +01:00
parent 75f356f4b2
commit 21e98fa81e
4 changed files with 13 additions and 9 deletions
@@ -16,7 +16,8 @@ True := by
  trivial

 Hint : True => "
-**Robo**  Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und bedingungslos wahr ist.
+**Robo**  Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und
+bedingungslos wahr ist.

 **Du** Und was genau ist dann zu beweisen?

@@ -27,9 +28,11 @@ Conclusion
 "
 **Schelm**  Wollte nur mal sehen, dass Ihr nicht auf den Kopf gefallen seid …

-**Du** *(zu Robo)*  Können wir nicht einfach immer dieses `trivial` verwenden?  Wie in einer Mathe-Vorlesung?
+**Du** *(zu Robo)*  Können wir nicht einfach immer dieses `trivial` verwenden?
+Wie in einer Mathe-Vorlesung?

-**Robo** Nein, das `trivial` hier hat eine ziemlich spezielle Bedeutung.  Das funktioniert nur in einer Handvoll Situationen.
+**Robo** Nein, das `trivial` hier hat eine ziemlich spezielle Bedeutung.
+Das funktioniert nur in einer Handvoll Situationen.
 "

 NewTactics trivial
@@ -16,7 +16,8 @@ Statement "" :
  trivial

 Hint : ¬False => "
-  **Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)` wahr ist, dann ist  `¬A` falsch, und umgekehrt.
+  **Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)`
+  wahr ist, dann ist  `¬A` falsch, und umgekehrt.

  **Du** Und `False` ist wahrscheinlich die Aussage, die immer falsch ist?

@@ -41,7 +41,7 @@ Statement ""
  assumption

 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."
+"**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."

 HiddenHint (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) =>
 "**Robo** Das `∧` im Goal kannst Du mit `constructor` zerlegen."
@@ -60,7 +60,7 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) =>
 "**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."

 HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) =>
-"**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
+"**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."

 -- TODO: Hint nur Anhand der Annahmen?