Merge pull request #931 from lean-ja/Seasawher/issue905

`<;>` の名前は？seqFocusでよいのか？

Examples/Tactic/SeqFocus.lean

@@ -1,5 +1,5 @@
 /- # <;>
-`<;>` (seq focus)は、直前のタクティクによって生成されたすべてのサブゴールに対して後続のタクティクを適用することを意味するタクティク結合子です。
+`<;>` は、直前のタクティクによって生成されたすべてのサブゴールに対して後続のタクティクを適用することを意味するタクティク結合子です。[^name]
 -/
 
 variable (P Q : Prop)
@@ -37,3 +37,5 @@ example (hP : P) (hQ : Q) (hR : R) : (P ∧ Q) ∧ R := by
 
   -- 証明完了
   done
+
+/- [^name]: `<;>` の正式な呼び名はわかりません。`linter.unnecessarySeqFocus` というリンタが存在するので、ここでは `seqFocus` と仮に呼んでいます。-/