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 de1c1f482cf91cd1cafbd54565cd119ae9c974df..052e00679c98ca5e5fef8018bc46d69d8b610f9b 100644 (file)
--- 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