From 1118162fa2c7b4dc860da0c3aa434bd2a1631855 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 16 Nov 2008 10:05:17 +0000 Subject: [PATCH] commented out unfinished proof --- .../matita/library/didactic/exercises/natural_deduction.ma | 2 ++ 1 file changed, 2 insertions(+) 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 -- 2.39.2