Added a new contrib div_and_mod and few modifs here and there.

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

diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma
index 835bb68734c397f2ae6bdbc1e6ef5ed0a1b22e18..a5aab65f5d16fb77eda84a18be88e163802a86d2 100644 (file)
--- a/helm/matita/library/logic/connectives.ma
+++ b/helm/matita/library/logic/connectives.ma
@@ -12,16 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/connectives/".
+set "baseuri" "cic:/matita/logic/connectives/".
 
 inductive True: Prop \def
 I : True.
 
-default "true" cic:/matita/logic/True.ind.
+default "true" cic:/matita/logic/connectives/True.ind.
 
 inductive False: Prop \def .
 
-default "false" cic:/matita/logic/False.ind.
+default "false" cic:/matita/logic/connectives/False.ind.
 
 definition Not: Prop \to Prop \def
 \lambda A. (A \to False).
@@ -30,7 +30,7 @@ theorem absurd : \forall A,C:Prop. A \to Not A \to C.
 intros. elim (H1 H).
 qed.
 
-default "absurd" cic:/matita/logic/absurd.ind.
+default "absurd" cic:/matita/logic/connectives/absurd.con.
 
 inductive And (A,B:Prop) : Prop \def
     conj : A \to B \to (And A B).