diff --git a/LeanByExample/Declarative/Inductive.lean b/LeanByExample/Declarative/Inductive.lean
index f8a5e71a..f71b896b 100644
--- a/LeanByExample/Declarative/Inductive.lean
+++ b/LeanByExample/Declarative/Inductive.lean
@@ -1,7 +1,7 @@
 /- # inductive
-`inductive` コマンドは、帰納型(inductive type)を定義することができます。
+`inductive` コマンドは、**帰納型(inductive type)** を定義することができます。
 
-帰納型とは、有限個のコンストラクタで構成され、すべての項がいずれかのコンストラクタで構成されることやコンストラクタの像が重ならないことなど、帰納的構成が満たすべきルールが保証されているような型のことです。
+帰納型とは、Lean においてユーザが新しい型を定義するための主要な方法です。帰納型はその型の項を得るための有限個の関数（コンストラクタ）を組み合わせることによって定まります。コンストラクタがこれから定義しようとしている型自身を引数に含むことも許されるので、帰納型は再帰的な構造を持つことができます。
 
 ## 帰納型の例