From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 16 Nov 2008 10:05:17 +0000 (+0000)
Subject: commented out unfinished proof
X-Git-Tag: make_still_working~4545
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1118162fa2c7b4dc860da0c3aa434bd2a1631855;p=helm.git

commented out unfinished proof
---

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index de1c1f482..052e00679 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -42,6 +42,7 @@ apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
 	]
 qed.
 
+(*
 theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
 apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B));
 apply rule (⇒_i [H] (¬A ∨ ¬B));
@@ -70,3 +71,4 @@ apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B));
 	   apply rule (show EM);
 	   ]
 	]
+*)
\ No newline at end of file