Merge pull request #1266 from lean-ja/Seasawher/issue1265

「宣言的コマンド」「対話的コマンド」という用語が一般的でないことを注意する

LeanByExample/Declarative/README.lean

@@ -3,6 +3,6 @@
 トップレベルコマンドには `#` から始まるものとそうでないものがあり、そうでないものを本書では便宜的に「宣言的コマンド」と呼んでいます。これは、そうしたコマンドが定義を行ったり属性を付与したりと、Lean に何かを宣言するために使われることが多いためです。
 
 ```admonish warning title="注意"
-宣言的コマンド(declarative command)という用語は Lean コミュニティでは通じると思いますが、一般的なものではありません。
+宣言的コマンド(declarative command)という用語は一般的なものではなく、著者が本書で使うために考案したものです。
 ```
 -/