X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FRELATIONAL-ARITHMETICS%2Fadd_defs.ma;h=77d6921a97a943a722bb1420c16f2ddcde33e3c9;hb=9ed9bdd5f158f092114c2d98c2537a9396d6a8d7;hp=4f95ad4e85e4c6daaa8d979c389d82fe34a1e099;hpb=110578d269f4ced34c4317eed5171a7f45884c15;p=helm.git

diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma b/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma
index 4f95ad4e8..77d6921a9 100644
--- a/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma
+++ b/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).
-