From 69e817b7e8ce6fe76772f895208998ed5d8337b9 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 19 Feb 2025 11:27:54 +0100
Subject: [PATCH] fixes

---
 .../Solutions/Topics/ClassicalPropositionalLogic.lean       | 6 +++---
 .../Solutions/Topics/IntuitionisticPropositionalLogic.lean  | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean b/GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean
index ce3ff67..e954986 100644
--- a/GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean
+++ b/GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean
@@ -55,17 +55,17 @@ def Valid (A : Formula) : Prop := ∅ ⊨ A
   using theorems tagged with `@[simp]`. -/
 
 variable {v : Variable → Prop} {A B : Formula}
-@[simp] lemma isTrue_neg : IsTrue v ~A ↔ ¬ IsTrue v A := by simp
+@[simp] lemma isTrue_neg : IsTrue v ~A ↔ ¬ IsTrue v A := by simp [neg]
 
 @[simp] lemma isTrue_top : IsTrue v ⊤ := by {
   -- sorry
-  simp
+  simp [top]
   -- sorry
 }
 
 @[simp] lemma isTrue_equiv : IsTrue v (A ⇔ B) ↔ (IsTrue v A ↔ IsTrue v B) := by {
   -- sorry
-  simp
+  simp [equiv]
   tauto
   -- sorry
 }
diff --git a/GlimpseOfLean/Solutions/Topics/IntuitionisticPropositionalLogic.lean b/GlimpseOfLean/Solutions/Topics/IntuitionisticPropositionalLogic.lean
index d3debcd..1ff9c1f 100644
--- a/GlimpseOfLean/Solutions/Topics/IntuitionisticPropositionalLogic.lean
+++ b/GlimpseOfLean/Solutions/Topics/IntuitionisticPropositionalLogic.lean
@@ -62,18 +62,18 @@ def Valid (A : Formula) : Prop := ∅ ⊨ A
   using theorems tagged with `@[simp]`. -/
 
 variable {v : Variable → H} {A B : Formula}
-@[simp] lemma eval_neg : eval v ~A = (eval v A)ᶜ := by simp
+@[simp] lemma eval_neg : eval v ~A = (eval v A)ᶜ := by simp [neg]
 
 @[simp] lemma eval_top : eval v top = ⊤ := by {
   -- sorry
-  simp
+  simp [top]
   -- sorry
 }
 
 @[simp]
 lemma isTrue_equiv : eval v (A ⇔ B) = (eval v A ⇨ eval v B) ⊓ (eval v B ⇨ eval v A) := by {
   -- sorry
-  simp
+  simp [equiv]
   -- sorry
 }