X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FRELATIONAL-ARITHMETICS%2Fadd_defs.ma;h=77d6921a97a943a722bb1420c16f2ddcde33e3c9;hb=cc3ab906b631ef0edb4402cb622fc3fa96682717;hp=4f95ad4e85e4c6daaa8d979c389d82fe34a1e099;hpb=389b29d17694ba6abe79dfd36d862321e05d17d6;p=helm.git

diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma
index 4f95ad4e8..77d6921a9 100644
--- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma
+++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma
@@ -19,4 +19,3 @@ include "nat_defs.ma".
 inductive add (p:nat): nat \to nat \to Prop \def
    | add_O_2: add p O p
    | add_S_2: \forall q, r. add p q r \to add p (S q) (S r).
-