From bfb1d0076c4adf923f0507e4e2ab26519e689b88 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 15 Nov 2008 15:15:46 +0000 Subject: [PATCH] Another bug. --- .../matita/library/didactic/exercises/natural_deduction.ma | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma index 2fef599e7..c26fcb6e8 100644 --- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma +++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma @@ -24,7 +24,7 @@ theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B. apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B)); apply rule (⇒_i [H] (¬A ∨ ¬B)); apply rule (RAA [K] (⊥)); -apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬C)); - [ apply rule (discharge [H]). - | +apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B)); + [ apply rule (discharge [K]). + | apply rule (∨_i_l (¬A)); ] -- 2.39.2