patched

[helm.git] / matita / contribs / RELATIONAL-ARITHMETICS / add_defs.ma

diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma b/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma
index 4f95ad4e85e4c6daaa8d979c389d82fe34a1e099..77d6921a97a943a722bb1420c16f2ddcde33e3c9 100644 (file)
--- 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).
-