From 389c47134aa9eb80895207614984b8b12fe24424 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 15 Nov 2008 15:13:38 +0000
Subject: [PATCH] This commit shows a bug.

---
 .../library/didactic/exercises/natural_deduction.ma    | 10 +++++++---
 1 file changed, 7 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 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]).
+	|
+	]
-- 
2.39.2