New command default "foo" uri1 ... urin

[helm.git] / helm / matita / library / logic.ma

diff --git a/helm/matita/library/logic.ma b/helm/matita/library/logic.ma
index a509bbb8da525c531c70e966b0c415533fab555d..fd37443965f85594e5cde7e491924c8133155954 100644 (file)
--- 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).