From 9c64b2e60746b2a2d8ada6f81317e11dbd4bf8bf Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 13 Oct 2024 20:33:28 +0900
Subject: [PATCH] =?UTF-8?q?local=20=E3=81=AE=E8=BF=BD=E5=8A=A0=E6=BC=8F?=
 =?UTF-8?q?=E3=82=8C=E4=BF=AE=E6=AD=A3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Reference/Declarative/AddAesopRules.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanByExample/Reference/Declarative/AddAesopRules.lean b/LeanByExample/Reference/Declarative/AddAesopRules.lean
index f647746..45af772 100644
--- a/LeanByExample/Reference/Declarative/AddAesopRules.lean
+++ b/LeanByExample/Reference/Declarative/AddAesopRules.lean
@@ -224,7 +224,7 @@ example (a b : Nat) (h : 3 ∣ (10 * a + b)) : 3 ∣ (a + b) := by
   omega
 
 -- aesop にルールを登録する
-add_aesop_rules safe tactic [(by omega)]
+local add_aesop_rules safe tactic [(by omega)]
 
 example (a b : Nat) (h : 3 ∣ (10 * a + b)) : 3 ∣ (a + b) := by
   -- aesop で証明できるようになった!