X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flogic.ma;fp=matita%2Fmatita%2Flib%2Fbasics%2Flogic.ma;h=b6a5d59b7e09a575ab43c3361cc33a0ae28eafdf;hb=bc477154d15f6979c948f9af602199af547d193e;hp=70e743e993ac96c12cdbf7a4a56cdc23bc8280b6;hpb=791b0dc201a023e772e4ba5c3da697c5ae271405;p=helm.git

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 70e743e99..b6a5d59b7 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -91,17 +91,21 @@ unification hint 0 ≔ T,a,b;
 inductive True: Prop ≝  
 I : True.
 
+interpretation "logical true" 'true = True.
+
 inductive False: Prop ≝ .
 
+interpretation "logical false" 'false = False.
+
 (* ndefinition Not: Prop → Prop ≝
-λA. A → False. *)
+λA. A → ⊥. *)
 
 inductive Not (A:Prop): Prop ≝
-nmk: (A → False) → Not A.
+nmk: (A → ⊥) → Not A.
 
 interpretation "logical not" 'not x = (Not x).
 
-theorem absurd : ∀A:Prop. A → ¬A → False.
+theorem absurd : ∀A:Prop. A → ¬A → ⊥.
 #A #H #Hn (elim Hn); /2/; qed.
 
 (*