diff --git a/server/adam/Adam/Doc/Tactics.lean b/server/adam/Adam/Doc/Tactics.lean index 665e402..5e1978a 100644 --- a/server/adam/Adam/Doc/Tactics.lean +++ b/server/adam/Adam/Doc/Tactics.lean @@ -446,6 +446,11 @@ Wenn das Goal von der Form `A ∨ B` ist, enscheidet man mit `right` die rechte * `left` entscheidet sich für die linke Seite. " +TacticDoc ring_nf +"\"ring Normal Form\": Identisch zu `ring`. `ring` wird geschrieben, wenn die Taktik das Goal schliesst, `ring_nf` +wenn man diese innerhalb eines Taktikblockes brauchen will. +" + TacticDoc ring " Löst Gleichungen mit den Operationen `+, -, *, ^`. diff --git a/server/adam/Adam/Levels/Predicate/L01_Ring.lean b/server/adam/Adam/Levels/Predicate/L01_Ring.lean index 80d1876..39d000c 100644 --- a/server/adam/Adam/Levels/Predicate/L01_Ring.lean +++ b/server/adam/Adam/Levels/Predicate/L01_Ring.lean @@ -27,4 +27,5 @@ Statement (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by Conclusion "" -NewTactic ring +-- TODO: Modifiy ring so it does not show info about using ring_nf. +NewTactic ring ring_nf