diff --git a/LeanByExample/Reference/Attribute/README.lean b/LeanByExample/Reference/Attribute/README.lean index 10527cc3..9d7e0836 100644 --- a/LeanByExample/Reference/Attribute/README.lean +++ b/LeanByExample/Reference/Attribute/README.lean @@ -2,5 +2,5 @@ 属性は、`attribute [foo] bar` または `@[foo]` という構文で使用することができます。 -Mathlib において利用可能な属性の一覧は [attribute list](https://seasawher.github.io/mathlib4-tactics/attributes.html) で確認できます。 +Mathlib において利用可能な属性の一覧は [attribute list](https://seasawher.github.io/mathlib4-help/attributes.html) で確認できます。 -/ diff --git a/LeanByExample/Reference/Tactic/README.lean b/LeanByExample/Reference/Tactic/README.lean index b4a0174b..d41c2d33 100644 --- a/LeanByExample/Reference/Tactic/README.lean +++ b/LeanByExample/Reference/Tactic/README.lean @@ -3,5 +3,5 @@ このセクションでは、Lean の組み込みのタクティクに加えて、Mathlib というライブラリで提供されているタクティクも紹介します。Mathlib には特定の分野に特化した強力な自動化タクティクがいくつもあり、数学理論の形式化をする上で欠かせません。 -なおこのリストは全部のタクティクを網羅していません。Mathlib の全タクティクのリストが必要であれば [mathlib4 tactics](https://seasawher.github.io/mathlib4-tactics/tactics.html) を参照してください。 +なおこのリストは全部のタクティクを網羅していません。Mathlib の全タクティクのリストが必要であれば [mathlib4 tactics](https://seasawher.github.io/mathlib4-help/tactics.html) を参照してください。 -/