X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2FPlogic%2Fconnectives.ma;h=491657676a85ada0ae073947190306fedbb0af87;hb=63b1b044e54bac3ffecc02ee2941b60f58b0c837;hp=d840143e3835ca29080b6b51eb0542690a84762f;hpb=ffdcaed2ae52b27119d8d8b16eda1a28a0aac82a;p=helm.git

diff --git a/helm/software/matita/nlibrary/Plogic/connectives.ma b/helm/software/matita/nlibrary/Plogic/connectives.ma
index d840143e3..491657676 100644
--- a/helm/software/matita/nlibrary/Plogic/connectives.ma
+++ b/helm/software/matita/nlibrary/Plogic/connectives.ma
@@ -23,18 +23,25 @@ ninductive False: Prop ≝ .
 
 default "false" cic:/matita/basics/connectives/False.ind.
 
+(*
 ndefinition Not: Prop → Prop ≝
-λA. A → False.
+λA. A → False. *)
+
+ninductive Not (A:Prop): Prop ≝
+nmk: (A → False) → Not A.
 
 interpretation "logical not" 'not x = (Not x).
 
+ntheorem absurd : ∀ A:Prop. A → ¬A → False.
+#A; #H; #Hn; nelim Hn;/2/; nqed.
+
+(*
 ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
 #A; #C; #H; #Hn; nelim (Hn H).
-nqed.
+nqed. *)
 
 ntheorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
-/3/.
-nqed.
+/4/; nqed.
 
 ninductive And (A,B:Prop) : Prop ≝
     conj : A → B → And A B.