X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Flibrary%2Flogic.ma;h=fd37443965f85594e5cde7e491924c8133155954;hb=b84c60ff48a21a62a08e636f32cf0df46dfbe45a;hp=a509bbb8da525c531c70e966b0c415533fab555d;hpb=109ddb8c437013d6d86e1564d5df3f8b089b9700;p=helm.git

diff --git a/helm/matita/library/logic.ma b/helm/matita/library/logic.ma
index a509bbb8d..fd3744396 100644
--- a/helm/matita/library/logic.ma
+++ b/helm/matita/library/logic.ma
@@ -18,8 +18,12 @@ set "baseuri" "cic:/matita/logic/".
 inductive True: Prop \def
 I : True.
 
+default "true" cic:/matita/logic/True.ind.
+
 inductive False: Prop \def .
 
+default "false" cic:/matita/logic/False.ind.
+
 definition Not: Prop \to Prop \def
 \lambda A. (A \to False).
 
@@ -27,6 +31,8 @@ theorem absurd : \forall A,C:Prop. A \to Not A \to C.
 intros. elim (H1 H).
 qed.
 
+default "absurd" cic:/matita/logic/absurd.ind.
+
 inductive And (A,B:Prop) : Prop \def
     conj : A \to B \to (And A B).