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

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index b6a5d59b7..70e743e99 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -91,21 +91,17 @@ 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 → ⊥. *)
+λA. A → False. *)
 
 inductive Not (A:Prop): Prop ≝
-nmk: (A → ⊥) → Not A.
+nmk: (A → False) → Not A.
 
 interpretation "logical not" 'not x = (Not x).
 
-theorem absurd : ∀A:Prop. A → ¬A → ⊥.
+theorem absurd : ∀A:Prop. A → ¬A → False.
 #A #H #Hn (elim Hn); /2/; qed.
 
 (*