From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 15 Nov 2008 15:15:46 +0000 (+0000)
Subject: Another bug.
X-Git-Tag: make_still_working~4554
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bfb1d0076c4adf923f0507e4e2ab26519e689b88;p=helm.git

Another bug.
---

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));
 	]