From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 15 Nov 2008 15:13:38 +0000 (+0000)
Subject: This commit shows a bug.
X-Git-Tag: make_still_working~4555
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=389c47134aa9eb80895207614984b8b12fe24424;p=helm.git

This commit shows a bug.
---

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 8ec8d6fd7..2fef599e7 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -21,6 +21,10 @@ include "didactic/support/natural_deduction.ma".
 
 
 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]).
+	|
+	]