we added the standard notation for True and False (logical constants)

[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 70e743e993ac96c12cdbf7a4a56cdc23bc8280b6..b6a5d59b7e09a575ab43c3361cc33a0ae28eafdf 100644 (file)
--- 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.
 
 (*