diff --git a/GLOSSARY.md b/GLOSSARY.md
index aa9bd53..4df7c4d 100644
--- a/GLOSSARY.md
+++ b/GLOSSARY.md
@@ -43,6 +43,7 @@
 | constructor | コンストラクタ | |
 | content | 内容 | |
 | context | （プログラム中のcontextの意で）コンテキスト、（文章中のcontextの意で）文脈 | |
+| conversion | 変換 | |
 | core language | コア言語 | |
 | core type theory | コア型理論 | |
 | curly brace | 波括弧 | |
@@ -253,6 +254,7 @@
 | trivial | 自明な | |
 | trust | 信頼 | |
 | tuple | タプル | |
+| turnstile | ターンスタイル | |
 | type class | 型クラス | |
 | type class instance synthesis | 型クラスインスタンス合成 | |
 | type signature | 型シグネチャ | |
diff --git a/Manual/Tactics/Conv.lean b/Manual/Tactics/Conv.lean
index a9e38b2..bc9297d 100644
--- a/Manual/Tactics/Conv.lean
+++ b/Manual/Tactics/Conv.lean
@@ -17,25 +17,46 @@ set_option pp.rawOnError true
 
 set_option linter.unusedVariables false
 
+/-
 #doc (Manual) "Targeted Rewriting with {tactic}`conv`" =>
+-/
+#doc (Manual) "{tactic}`conv` によるターゲットの書き換え（Targeted Rewriting with {tactic}`conv` ）" =>
 
 
+:::comment
 The {tactic}`conv`, or conversion, tactic allows targeted rewriting within a goal.
 The argument to {tactic}`conv` is written in a separate language that interoperates with the main tactic language; it features commands to navigate to specific subterms within the goal along with commands that allow these subterms to be rewritten.
 {tactic}`conv` is useful when rewrites should only be applied in part of a goal (e.g. only on one side of an equality), rather than across the board, or when rewrites should be applied underneath a binder that prevents tactics like {tactic}`rw` from accessing the term.
 
+:::
+
+{tactic}`conv` 、もしくは変換タクティクはゴール内のターゲットを絞った書き換えを可能にします。 {tactic}`conv` の引数はメインのタクティク言語と相互に連携する別の言語で記述されます；これはゴール内の特定の部分項に移動するコマンドと、これらの部分項を書き換えるコマンドを備えています。 {tactic}`conv` は書き換えをゴール全体ではなく、ゴールの一部（例えば等式の片側のみ）にのみ適用する場合や、 {tactic}`rw` のようなタクティクが項にアクセスするのを防いでしまう束縛子の中の書き換えを適用する場合に便利です。
+
+:::comment
 The conversion tactic language is very similar to the main tactic language: it uses the same proof states, tactics work primarily on the main goal and may either fail or succeed with a sequence of new goals, and macro expansion is interleaved with tactic execution.
 Unlike the main tactic language, in which tactics are intended to eventually solve goals, the {tactic}`conv` tactic is used to _change_ a goal so that it becomes amenable to further processing in the main tactic language.
 Goals that are intended to be rewritten with {tactic}`conv` are shown with a vertical bar instead of a turnstile.
 
+:::
+
+変換タクティク言語はメインのタクティク言語に非常に似ています：同じ証明状態を使用し、タクティクは主にメインゴールに対して作用し、新しいゴールの列で失敗または成功する可能性があり、マクロ展開はタクティクの実行と交互に行われます。タクティクが最終的にゴールを解決するためのものであるメインのタクティク言語とは異なり、 {tactic}`conv` はゴールを _変更_ するために用いられます。これによってゴールはその後のメインのタクティク言語で容易に処理できるようになります。 {tactic}`conv` で書き換えることを意図しているゴールはターンスタイルの代わりに縦棒で表示されます。
+
 :::tactic "conv"
 :::
 
-::::example "Navigation and Rewriting with {tactic}`conv`"
+:::comment
+::example "Navigation and Rewriting with {tactic}`conv`"
+:::
+::::example "{tactic}`conv` による移動と書き換え"
 
+:::comment
 In this example, there are multiple instances of addition, and {tactic}`rw` would by default rewrite the first instance that it encounters.
 Using {tactic}`conv` to navigate to the specific subterm before rewriting leaves {tactic}`rw` no choice but to rewrite the correct term.
 
+:::
+
+この例では、加算のインスタンスが複数存在し、 {tactic}`rw` はデフォルトで最初に出会ったインスタンスを書き換えてしまいます。書き換える前に特定の部分項へ移動するために {tactic}`conv` を使用すると、 {tactic}`rw` は正しい項を書き換える以外に選択肢がなくなります。
+
 ```lean
 example (x y z : Nat) : x + (y + z) = (x + z) + y := by
   conv =>
@@ -47,13 +68,21 @@ example (x y z : Nat) : x + (y + z) = (x + z) + y := by
 
 ::::
 
-::::example "Rewriting Under Binders with {tactic}`conv`"
+:::comment
+::example "Rewriting Under Binders with {tactic}`conv`"
+:::
+::::example "{tactic}`conv` による束縛子の中の書き換え"
 
+:::comment
 In this example, addition occurs under binders, so {tactic}`rw` can't be used.
 However, after using {tactic}`conv` to navigate to the function body, it succeeds.
 The nested use of {tactic}`conv` causes control to return to the current position in the term after performing further coversions on one of its subterms.
 Because the goal is a reflexive equation after rewriting, {tactic}`conv` automatically closes it.
 
+:::
+
+この例では、加算は束縛子の中に存在するため、 {tactic}`rw` は使えません。しかし、 {tactic}`conv` を使用して関数本体に移動すると成功します。入れ子になった {tactic}`conv` の使用は、その部分項の1つに対してさらなる変換を実行したのち、制御を項の中の現在の位置に戻します。ゴールは書き換え後の反射性の等式であるため、 {tactic}`conv` は自動的にこれを閉じます。
+
 ```lean
 example : (fun (x y z : Nat) => x + (y + z)) = (fun x y z => (z + x) + y) := by
   conv =>
@@ -69,9 +98,14 @@ example : (fun (x y z : Nat) => x + (y + z)) = (fun x y z => (z + x) + y) := by
 
 ::::
 
+:::comment
 # Control Structures
 
 
+:::
+
+# 制御構造（Control Structures）
+
 :::conv first show := "first"
 :::
 
@@ -96,8 +130,13 @@ example : (fun (x y z : Nat) => x + (y + z)) = (fun x y z => (z + x) + y) := by
 :::conv convDone show:= "done"
 :::
 
+:::comment
 # Goal Selection
 
+:::
+
+# ゴールの選択（Goal Selection）
+
 :::conv allGoals show:= "all_goals"
 :::
 
@@ -126,8 +165,13 @@ example : (fun (x y z : Nat) => x + (y + z)) = (fun x y z => (z + x) + y) := by
 :::
 
 
+:::comment
 # Navigation
 
+:::
+
+# 移動（Navigation）
+
 :::conv lhs show:= "lhs"
 :::
 
@@ -177,9 +221,19 @@ $x:ident
 :::conv convIntro___ show := "intro"
 :::
 
+:::comment
 # Changing the Goal
+:::
+
+# ゴールの変更（Changing the Goal）
+
+:::comment
 ## Reduction
 
+:::
+
+## 簡約（Reduction）
+
 :::conv whnf show:= "whnf"
 :::
 
@@ -195,7 +249,12 @@ $x:ident
 :::conv unfold show:= "unfold"
 :::
 
+:::comment
 ## Simplification
+:::
+
+## 単純化（Simplification）
+
 :::conv simp show:= "simp"
 :::
 
@@ -205,9 +264,14 @@ $x:ident
 :::conv simpMatch show:= "simp_match"
 :::
 
+:::comment
 ## Rewriting
 
 
+:::
+
+## 書き換え（Rewriting）
+
 :::conv change show:= "change"
 :::
 
@@ -224,8 +288,13 @@ $x:ident
 :::
 
 
+:::comment
 # Nested Tactics
 
+:::
+
+# 入れ子のタクティク（Nested Tactics）
+
 :::tactic Lean.Parser.Tactic.Conv.convTactic
 :::
 
@@ -242,14 +311,24 @@ $x:ident
 :::
 
 
+:::comment
 # Debugging Utilities
 
+:::
+
+# デバッグ用ユーティリティ（Debugging Utilities）
+
 :::conv convTrace_state show:= "trace_state"
 :::
 
 
+:::comment
 # Other
 
+:::
+
+# その他（Other）
+
 :::conv convRfl show:= "rfl"
 :::
 
diff --git a/Manual/Tactics/Reference.lean b/Manual/Tactics/Reference.lean
index 7db9af5..b3a0511 100644
--- a/Manual/Tactics/Reference.lean
+++ b/Manual/Tactics/Reference.lean
@@ -18,19 +18,31 @@ set_option pp.rawOnError true
 
 set_option linter.unusedVariables false
 
+/-
 #doc (Manual) "Tactic Reference" =>
+-/
+#doc (Manual) "タクティクリファレンス（Tactic Reference）" =>
 
-
+:::comment
 # Assumptions
 
+:::
+
+# 仮定（Assumptions）
+
 :::tactic Lean.Parser.Tactic.assumption
 :::
 
 :::tactic "apply_assumption"
 :::
 
+:::comment
 # Quantifiers
 
+:::
+
+# 量化子（Quantifiers）
+
 :::tactic "exists"
 :::
 
@@ -48,8 +60,13 @@ set_option linter.unusedVariables false
 :::
 
 
+:::comment
 # Relations
 
+:::
+
+# 関係（Relations）
+
 :::planned 47
  * Descriptions of the `symm` and `refl` and `trans` attributes
 :::
@@ -75,8 +92,13 @@ set_option linter.unusedVariables false
 :::
 
 
+:::comment
 ## Equality
 
+:::
+
+## 等価性（Equality）
+
 :::tactic "subst"
 :::
 
@@ -95,8 +117,13 @@ set_option linter.unusedVariables false
 :::tactic "ac_rfl"
 :::
 
+:::comment
 # Lemmas
 
+:::
+
+# 補題（Lemmas）
+
 :::tactic "exact"
 :::
 
@@ -116,8 +143,13 @@ set_option linter.unusedVariables false
 :::tactic "apply_rules"
 :::
 
+:::comment
 # Falsehood
 
+:::
+
+# 偽（Falsehood）
+
 :::tactic "exfalso"
 :::
 
@@ -128,8 +160,13 @@ set_option linter.unusedVariables false
 :::
 
 
+:::comment
 # Goal Management
 
+:::
+
+# ゴールの管理（Goal Management）
+
 :::tactic "suffices"
 :::
 
@@ -155,11 +192,21 @@ set_option linter.unusedVariables false
 :::
 
 
+:::comment
 # Cast Management
 
+:::
+
+# キャストの管理（Cast Management）
+
+:::comment
 The tactics in this section make it easier avoid getting stuck on {deftech}_casts_, which are functions that coerce data from one type to another, such as converting a natural number to the corresponding integer.
 They are described in more detail in [_Simplifying Casts and Coercions_](https://arxiv.org/abs/2001.10594) by Robert Y. Lewis and Paul-Nicolas Madelaine.
 
+:::
+
+本節のタクティクは {deftech}_キャスト_ （cast）に詰まってしまうことを回避します。キャストとはある型から別の型にデータを強制する関数であり、例えば自然数を対応する整数に変換するようなものです。これらは Robert Y. Lewis と Paul-Nicolas Madelaine による [_Simplifying Casts and Coercions_](https://arxiv.org/abs/2001.10594) で詳しく説明されています。
+
 :::tactic Lean.Parser.Tactic.tacticNorm_cast_
 :::
 
@@ -181,9 +228,14 @@ They are described in more detail in [_Simplifying Casts and Coercions_](https:/
 
 
 
+:::comment
 # Extensionality
 
 
+:::
+
+# 外延性（Extensionality）
+
 :::tactic "ext"
 :::
 
@@ -198,8 +250,13 @@ They are described in more detail in [_Simplifying Casts and Coercions_](https:/
 
 {include 0 Manual.Tactics.Reference.Simp}
 
+
+# 書き換え（Rewriting）
+
+:::comment
 # Rewriting
 
+:::
 :::tactic "rw"
 :::
 
@@ -233,10 +290,20 @@ Implemented by {name}`Lean.Elab.Tactic.evalUnfold`.
 :::
 
 
+:::comment
 # Inductive Types
 
+:::
+
+# 帰納型（Inductive Types）
+
+:::comment
 ## Introduction
 
+:::
+
+## 帰納法（Introduction）
+
 :::tactic "constructor"
 :::
 
@@ -253,8 +320,14 @@ Implemented by {name}`Lean.Elab.Tactic.evalUnfold`.
 :::tactic "right"
 :::
 
+:::comment
 ## Elimination
 
+:::
+
+## 除去（Elimination）
+
+
 :::planned 48
 
 Description of the `@[induction_eliminator]` and `@[cases_eliminator]` attributes
@@ -277,12 +350,22 @@ Description of the `@[induction_eliminator]` and `@[cases_eliminator]` attribute
 :::
 
 
+:::comment
 # Library Search
 
+:::
+
+# ライブラリ検索（Library Search）
+
+:::comment
 The library search tactics are intended for interactive use.
 When run, they search the Lean library for lemmas or rewrite rules that could be applicable in the current situation, and suggests a new tactic.
 These tactics should not be left in a proof; rather, their suggestions should be incorporated.
 
+:::
+
+ライブラリ検索タクティクは対話的な使用を目的としています。これらを実行すると、Lean ライブラリ内を検索し、現在の状況に適用できそうな補題や書き換え規則を探し、新しいタクティクを提案します。これらのタクティクは証明の中に放置されるべきではなく、むしろその提案を受け入れるべきです。
+
 :::tactic "exact?"
 :::
 
@@ -292,12 +375,17 @@ These tactics should not be left in a proof; rather, their suggestions should be
 
 
 
-:::tacticExample
+::::tacticExample
 {goal show:=false}`∀ (i j k : Nat), i < j → j < k → i < k`
 ```setup
 intro i j k h1 h2
 ```
+:::comment
 In this proof state:
+:::
+
+この証明状態において：
+
 ```pre
 i j k : Nat
 h1 : i < j
@@ -305,8 +393,13 @@ h2 : j < k
 ⊢ i < k
 ```
 
+:::comment
 invoking {tacticStep}`apply?` suggests:
 
+:::
+
+{tacticStep}`apply?` の実行結果は以下を提案します：
+
 ```tacticOutput
 Try this: exact Nat.lt_trans h1 h2
 ```
@@ -314,22 +407,32 @@ Try this: exact Nat.lt_trans h1 h2
 ```post (show := false)
 
 ```
-:::
+::::
 
 
 :::tactic "rw?"
 :::
 
+:::comment
 # Case Analysis
 
+:::
+
+# ケース分析（Case Analysis）
+
 :::tactic "split"
 :::
 
 :::tactic "by_cases"
 :::
 
+:::comment
 # Decision Procedures
 
+:::
+
+# 決定処理（Decision Procedures）
+
 :::tactic Lean.Parser.Tactic.decide show:="decide"
 :::
 
@@ -343,9 +446,14 @@ Try this: exact Nat.lt_trans h1 h2
 :::
 
 
+:::comment
 ## SAT Solver Integration
 
 
+:::
+
+## SAT ソルバの統合（SAT Solver Integration）
+
 :::tactic "bv_decide"
 :::
 
@@ -358,8 +466,13 @@ Try this: exact Nat.lt_trans h1 h2
 :::tactic Lean.Parser.Tactic.bvTrace
 :::
 
+:::comment
 # Control Flow
 
+:::
+
+# フロー制御（Control Flow）
+
 :::tactic "skip"
 :::
 
@@ -390,10 +503,20 @@ Try this: exact Nat.lt_trans h1 h2
 :::
 
 
+:::comment
 # Term Elaboration Backends
 
+:::
+
+# 項エラボレーションのバックエンド（Term Elaboration Backends）
+
+:::comment
 These tactics are used during elaboration of terms to satisfy obligations that arise.
 
+:::
+
+これらのタクティクは項のエラボレーション中において発生した義務を満たすために用いられます。
+
 :::tactic "decreasing_tactic"
 :::
 
@@ -414,8 +537,13 @@ These tactics are used during elaboration of terms to satisfy obligations that a
 
 
 
+:::comment
 # Debugging Utilities
 
+:::
+
+# デバッグ用ユーティリティ（Debugging Utilities）
+
 :::tactic "sorry"
 :::
 
@@ -432,8 +560,13 @@ These tactics are used during elaboration of terms to satisfy obligations that a
 :::
 
 
+:::comment
 # Other
 
+:::
+
+# その他（Other）
+
 :::tactic "trivial"
 :::
 
diff --git a/Manual/Tactics/Reference/Simp.lean b/Manual/Tactics/Reference/Simp.lean
index f29099d..fc8316a 100644
--- a/Manual/Tactics/Reference/Simp.lean
+++ b/Manual/Tactics/Reference/Simp.lean
@@ -16,14 +16,22 @@ set_option pp.rawOnError true
 
 set_option linter.unusedVariables false
 
+/-
 #doc (Manual) "Simplification" =>
+-/
+#doc (Manual) "単純化（Simplification）" =>
 
 %%%
 tag := "simp-tactics"
 %%%
 
+:::comment
 The simplifier is described in greater detail in {ref "the-simplifier"}[its dedicated chapter].
 
+:::
+
+単純化器については {ref "the-simplifier"}[専用の章] で詳細に説明します。
+
 :::tactic "simp"
 :::