basic lemmas

[helm.git] / matita / matita / lib / basics / logic.ma

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index b6a5d59b7e09a575ab43c3361cc33a0ae28eafdf..70e743e993ac96c12cdbf7a4a56cdc23bc8280b6 100644 (file)
--- 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.
 
 (*